let L be non empty lower-bounded Poset; :: thesis: for F being Filter of L holds

( F is proper iff not Bottom L in F )

let F be Filter of L; :: thesis: ( F is proper iff not Bottom L in F )

then F <> the carrier of L ;

hence F is proper ; :: thesis: verum

( F is proper iff not Bottom L in F )

let F be Filter of L; :: thesis: ( F is proper iff not Bottom L in F )

hereby :: thesis: ( not Bottom L in F implies F is proper )

assume
not Bottom L in F
; :: thesis: F is proper assume
F is proper
; :: thesis: not Bottom L in F

then F <> the carrier of L ;

then consider a being object such that

A1: ( ( a in F & not a in the carrier of L ) or ( a in the carrier of L & not a in F ) ) by TARSKI:2;

reconsider a = a as Element of L by A1;

a >= Bottom L by YELLOW_0:44;

hence not Bottom L in F by A1, WAYBEL_0:def 20; :: thesis: verum

end;then F <> the carrier of L ;

then consider a being object such that

A1: ( ( a in F & not a in the carrier of L ) or ( a in the carrier of L & not a in F ) ) by TARSKI:2;

reconsider a = a as Element of L by A1;

a >= Bottom L by YELLOW_0:44;

hence not Bottom L in F by A1, WAYBEL_0:def 20; :: thesis: verum

then F <> the carrier of L ;

hence F is proper ; :: thesis: verum