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 )
hereby :: thesis: ( not Bottom L in F implies 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;
assume not Bottom L in F ; :: thesis: F is proper
then F <> the carrier of L ;
hence F is proper ; :: thesis: verum