let X be non empty set ; :: thesis: for F being non empty Subset of (BooleLatt X) holds
( ( F is with_non-empty_elements & F is Filter of (BooleLatt X) ) iff F is Filter of X )
let F be non empty Subset of (BooleLatt X); :: thesis: ( ( F is with_non-empty_elements & F is Filter of (BooleLatt X) ) iff F is Filter of X )

hereby :: thesis: ( F is Filter of X implies ( F is with_non-empty_elements & F is Filter of (BooleLatt X) ) )

assume that
A1: F is with_non-empty_elements and
A2: F is Filter of (BooleLatt X) ; :: thesis: F is Filter of X
A3: F is non empty Subset-Family of X by LATTICE3:def 1;
for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) by A2, Th32;
hence F is Filter of X by A1, A3, CARD_FIL:def 1; :: thesis: verum

end;

assume F is Filter of X ; :: thesis: ( F is with_non-empty_elements & F is Filter of (BooleLatt X) )
then ( F is with_non-empty_elements & ( for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) ) ) by CARD_FIL:def 1;
hence ( F is with_non-empty_elements & F is Filter of (BooleLatt X) ) by Th32; :: thesis: verum