let X be set ; :: thesis: for F being Filter of (BoolePoset X) holds F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
let F be Filter of (BoolePoset X); :: thesis: F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
set Xs = { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ;
set RS = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))));
A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;
F in Filt (BoolePoset X) ;
then reconsider F9 = F as Element of (InclPoset (Filt (BoolePoset X))) by A1;
A2: { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } c= the carrier of (InclPoset (Filt (BoolePoset X)))

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } or p in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume p in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ; :: thesis: p in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex YY being Subset of X st
( p = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY ) } ,(InclPoset (Filt (BoolePoset X)))) & YY in F ) ;
hence p in the carrier of (InclPoset (Filt (BoolePoset X))) ; :: thesis: verum

end;

A3: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def 2
.= bool X by LATTICE3:def 1 ;

now :: thesis: not { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } is empty

consider YY being object such that
A4: YY in F by XBOOLE_0:def 1;
reconsider YY = YY as set by TARSKI:1;
"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY ) } ,(InclPoset (Filt (BoolePoset X)))) in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } by A3, A4;
hence not { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } is empty ; :: thesis: verum

end;

then reconsider Xs9 = { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A2;
A5: ex_sup_of Xs9, InclPoset (Filt (BoolePoset X)) by YELLOW_0:17;
F c= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in F or p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) )
assume A6: p in F ; :: thesis: p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
then reconsider Y = p as Element of F ;
set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
A7: "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } by A3;

per cases ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty or not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ) ;

suppose A8: { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ; :: thesis: p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))

A9: p in the carrier of (BoolePoset X) by A6;
Xs9 is_<=_than "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A5, YELLOW_0:def 9;
then A10: "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) <= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A7;
"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A8
.= bool X by WAYBEL16:15 ;
then bool X c= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A10, YELLOW_1:3;
hence p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A3, A9; :: thesis: verum

end;

suppose A11: not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ; :: thesis: p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))

{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; :: thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A1; :: thesis: verum

end;

then reconsider Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A11;
for yy being set st yy in Xsi holds
Y in yy

proof

reconsider Y9 = Y as Element of (BoolePoset X) ;
let yy be set ; :: thesis: ( yy in Xsi implies Y in yy )
assume yy in Xsi ; :: thesis: Y in yy
then consider r being Element of (BoolePoset X) such that
A12: yy = uparrow r and
A13: ex z being Element of X st
( r = {z} & z in Y ) ;
r c= Y by A13, ZFMISC_1:31;
then r <= Y9 by YELLOW_1:2;
hence Y in yy by A12, WAYBEL_0:18; :: thesis: verum

end;

then ( "/\" (Xsi,(InclPoset (Filt (BoolePoset X)))) = meet Xsi & Y in meet Xsi ) by SETFAM_1:def 1, WAYBEL16:10;
then A14: p in union { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } by A7, TARSKI:def 4;
union Xs9 c= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by WAYBEL16:17, YELLOW_0:17;
hence p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A14; :: thesis: verum

end;

end;

end;

then A15: F9 <= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3;
{ ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } is_<=_than F9

proof

let b be Element of (InclPoset (Filt (BoolePoset X))); :: according to LATTICE3:def 9 :: thesis: ( not b in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } or b <= F9 )
assume b in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ; :: thesis: b <= F9
then consider Y being Subset of X such that
A16: b = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) and
A17: Y in F ;
reconsider Y9 = Y as Element of F by A17;
set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;

per cases ( Y is empty or not Y is empty ) ;

suppose A18: Y is empty ; :: thesis: b <= F9

now :: thesis: { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty

assume not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ; :: thesis: contradiction
then consider p being object such that
A19: p in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by XBOOLE_0:def 1;
ex x being Element of (BoolePoset X) st
( p = uparrow x & ex z being Element of X st
( x = {z} & z in Y ) ) by A19;
hence contradiction by A18; :: thesis: verum

end;

then A20: "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X)))
.= bool X by WAYBEL16:15 ;
Bottom (BoolePoset X) = {} by YELLOW_1:18;
then uparrow (Bottom (BoolePoset X)) c= F by A17, A18, WAYBEL11:42;
then bool X c= F by A3, WAYBEL14:10;
hence b <= F9 by A3, A16, A20, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A21: not Y is empty ; :: thesis: b <= F9

A22: now :: thesis: not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty

consider z being object such that
A23: z in Y by A21, XBOOLE_0:def 1;
reconsider z = z as Element of X by A23;
reconsider x = {z} as Element of (BoolePoset X) by A3, A23, ZFMISC_1:31;
uparrow x in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by A23;
hence not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ; :: thesis: verum

end;

{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; :: thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A1; :: thesis: verum

end;

then reconsider Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A22;
A24: "/\" (Xsi,(InclPoset (Filt (BoolePoset X)))) = meet Xsi by WAYBEL16:10;
b c= F9

proof

let yy be object ; :: according to TARSKI:def 3 :: thesis: ( not yy in b or yy in F9 )
b in Filt (BoolePoset X) by A1;
then consider bf being Filter of (BoolePoset X) such that
A25: b = bf ;
assume A26: yy in b ; :: thesis: yy in F9
then reconsider yy9 = yy as Element of bf by A25;
reconsider yy9 = yy9 as Element of (BoolePoset X) ;
Y c= yy9

proof

let zz be object ; :: according to TARSKI:def 3 :: thesis: ( not zz in Y or zz in yy9 )
assume A27: zz in Y ; :: thesis: zz in yy9
then reconsider z = zz as Element of X ;
reconsider xz = {z} as Element of (BoolePoset X) by A3, A27, ZFMISC_1:31;
uparrow xz in Xsi by A27;
then yy in uparrow xz by A16, A24, A26, SETFAM_1:def 1;
then xz <= yy9 by WAYBEL_0:18;
then {z} c= yy9 by YELLOW_1:2;
hence zz in yy9 by ZFMISC_1:31; :: thesis: verum

end;

then Y9 <= yy9 by YELLOW_1:2;
then ( uparrow Y9 c= F9 & yy in uparrow Y9 ) by WAYBEL11:42, WAYBEL_0:18;
hence yy in F9 ; :: thesis: verum

end;

hence b <= F9 by YELLOW_1:3; :: thesis: verum

end;

end;

end;

then "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) <= F9 by A5, YELLOW_0:def 9;
hence F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A15, YELLOW_0:def 3; :: thesis: verum