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

.= bool X by LATTICE3:def 1 ;

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

( 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

( 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

( 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

A3: the carrier of (BoolePoset X) =
the carrier of (LattPOSet (BooleLatt X))
by YELLOW_1:def 2
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;( 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

.= 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

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 } 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;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

( 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

then A15:
F9 <= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
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;

end;( 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 ) ;

end;

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

( 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;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

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

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

( 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

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;( x = {z} & z in Y ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))

proof

then reconsider Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
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;( 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

( 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

then
( "/\" (Xsi,(InclPoset (Filt (BoolePoset X)))) = meet Xsi & Y in meet Xsi )
by SETFAM_1:def 1, WAYBEL16:10;
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;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

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

( 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

then
"\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
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 ) } ;

end;( 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 )
;

end;

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

( 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;

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

then A20: "/\" ( { (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;( 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

( 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

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

( x = {z} & z in Y ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))

( 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

end;

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

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

( x = {z} & z in Y ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))

proof

then reconsider Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
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;( 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

( 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

hence
b <= F9
by YELLOW_1:3; :: thesis: verum
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

then ( uparrow Y9 c= F9 & yy in uparrow Y9 ) by WAYBEL11:42, WAYBEL_0:18;

hence yy in F9 ; :: thesis: verum

end;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

then
Y9 <= yy9
by YELLOW_1:2;
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;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

then ( uparrow Y9 c= F9 & yy in uparrow Y9 ) by WAYBEL11:42, WAYBEL_0:18;

hence yy in F9 ; :: thesis: verum

( 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