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