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;
A2: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def 2
.= bool X by LATTICE3:def 1 ;
A3: { ("/\" { (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 set ; :: 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 consider YY being Subset of X such that
A4: 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))) and
YY in F ;
thus p in the carrier of (InclPoset (Filt (BoolePoset X))) by A4; :: thesis: verum

end;

now

consider YY being set such that
A5: YY in F by XBOOLE_0:def 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 A2, A5;
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 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 } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A3;
A6: ex_sup_of Xs', InclPoset (Filt (BoolePoset X)) by YELLOW_0:17;
F in Filt (BoolePoset X) ;
then reconsider F' = F as Element of (InclPoset (Filt (BoolePoset X))) by A1;
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 set ; :: 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 A7: 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 ) } ;
A8: "/\" { (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 A2;

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 { (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)))

then A9: "/\" { (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 ;
Xs' 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 A6, YELLOW_0:def 9;
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))) <= "\/" { ("/\" { (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 A8, LATTICE3:def 9;
then A10: 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 A9, YELLOW_1:3;
p in the carrier of (BoolePoset X) by A7;
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 A2, A10; :: 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 set ; :: 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 consider xz being Element of (BoolePoset X) such that
A12: r = uparrow xz and
ex z being Element of X st
( xz = {z} & z in Y ) ;
thus r in the carrier of (InclPoset (Filt (BoolePoset X))) by A1, A12; :: 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;
A13: "/\" Xsi,(InclPoset (Filt (BoolePoset X))) = meet Xsi by WAYBEL16:10;
for yy being set st yy in Xsi holds
Y in yy

proof

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
A14: yy = uparrow r and
A15: ex z being Element of X st
( r = {z} & z in Y ) ;
reconsider Y' = Y as Element of (BoolePoset X) ;
r c= Y by A15, ZFMISC_1:37;
then r <= Y' by YELLOW_1:2;
hence Y in yy by A14, WAYBEL_0:18; :: thesis: verum

end;

then Y in meet Xsi by SETFAM_1:def 1;
then A16: 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 A8, A13, TARSKI:def 4;
union Xs' 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 A6, WAYBEL16: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 A16; :: thesis: verum

end;

end;

end;

then A17: 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 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 F'

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 <= F' )
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 <= F'
then consider Y being Subset of X such that
A18: 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
A19: Y in F ;
reconsider Y' = Y as Element of F by A19;
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 A20: Y is empty ; :: thesis: b <= F'

now

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 set such that
A21: 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;
consider x being Element of (BoolePoset X) such that
p = uparrow x and
A22: ex z being Element of X st
( x = {z} & z in Y ) by A21;
consider z being Element of X such that
A23: ( x = {z} & z in Y ) by A22;
thus contradiction by A20, A23; :: thesis: verum

end;

then A24: "/\" { (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 A19, A20, WAYBEL11:42;
then bool X c= F by A2, WAYBEL14:10;
hence b <= F' by A2, A18, A24, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A25: not Y is empty ; :: thesis: b <= F'

A26: now

consider z being set such that
A27: z in Y by A25, XBOOLE_0:def 1;
reconsider z = z as Element of X by A27;
reconsider x = {z} as Element of (BoolePoset X) by A2, A27, ZFMISC_1:37;
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 A27;
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 set ; :: 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 consider xz being Element of (BoolePoset X) such that
A28: r = uparrow xz and
ex z being Element of X st
( xz = {z} & z in Y ) ;
thus r in the carrier of (InclPoset (Filt (BoolePoset X))) by A1, A28; :: 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 A26;
A29: "/\" Xsi,(InclPoset (Filt (BoolePoset X))) = meet Xsi by WAYBEL16:10;
b c= F'

proof

let yy be set ; :: according to TARSKI:def 3 :: thesis: ( not yy in b or yy in F' )
assume A30: yy in b ; :: thesis: yy in F'
b in Filt (BoolePoset X) by A1;
then consider bf being Filter of (BoolePoset X) such that
A31: b = bf ;
reconsider yy' = yy as Element of bf by A30, A31;
reconsider yy' = yy' as Element of (BoolePoset X) ;
A32: uparrow Y' c= F' by WAYBEL11:42;
Y c= yy'

proof

let zz be set ; :: according to TARSKI:def 3 :: thesis: ( not zz in Y or zz in yy' )
assume A33: zz in Y ; :: thesis: zz in yy'
then reconsider z = zz as Element of X ;
reconsider xz = {z} as Element of (BoolePoset X) by A2, A33, ZFMISC_1:37;
uparrow xz in Xsi by A33;
then yy in uparrow xz by A18, A29, A30, SETFAM_1:def 1;
then xz <= yy' by WAYBEL_0:18;
then {z} c= yy by YELLOW_1:2;
hence zz in yy' by ZFMISC_1:37; :: thesis: verum

end;

then Y' <= yy' by YELLOW_1:2;
then yy in uparrow Y' by WAYBEL_0:18;
hence yy in F' by A32; :: thesis: verum

end;

hence b <= F' 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))) <= F' by A6, 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 A17, YELLOW_0:def 3; :: thesis: verum