let X be non empty set ; :: thesis: for F being Filter of (BoolePoset X) holds F is Filter of (BooleLatt X)
let F be Filter of (BoolePoset X); :: thesis: F is Filter of (BooleLatt X)

now :: thesis: 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 ) )

let Y1, Y2 be Subset of X; :: thesis: ( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) )

hereby :: thesis: ( Y1 in F & Y1 c= Y2 implies Y2 in F )

assume that
A1: Y1 in F and
A2: Y2 in F ; :: thesis: Y1 /\ Y2 in F
reconsider Z1 = Y1, Z2 = Y2 as Element of (BoolePoset X) by LATTICE3:def 1;
A3: Z1 "/\" Z2 in F by A1, A2, WAYBEL_0:41;
set W = Z1 "/\" Z2;
reconsider Z1 = Z1, Z2 = Z2 as Element of (BooleLatt X) ;
thus Y1 /\ Y2 in F by A3, YELLOW_1:17; :: thesis: verum

end;

hereby :: thesis: verum

assume that
A4: Y1 in F and
A5: Y1 c= Y2 ; :: thesis: Y2 in F
reconsider Z1 = Y1, Z2 = Y2 as Element of (BoolePoset X) by LATTICE3:def 1;
Z1 <= Z2 by YELLOW_1:2, A5;
hence Y2 in F by A4, WAYBEL_0:def 20; :: thesis: verum

end;

end;

hence F is Filter of (BooleLatt X) by Th32; :: thesis: verum