let X be set ; :: thesis: for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L

for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds

h = f -extension_to_hom

let L be non empty complete continuous Poset; :: thesis: for f being Function of (FixedUltraFilters X), the carrier of L

for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds

h = f -extension_to_hom

let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds

h = f -extension_to_hom

let h be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; :: thesis: ( h | (FixedUltraFilters X) = f implies h = f -extension_to_hom )

assume A1: h | (FixedUltraFilters X) = f ; :: thesis: h = f -extension_to_hom

set F = f -extension_to_hom ;

set cL = the carrier of L;

set BP = BoolePoset X;

set IP = InclPoset (Filt (BoolePoset X));

set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));

A2: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;

reconsider F9 = f -extension_to_hom as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;

reconsider h9 = h as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;

A3: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def 2

.= bool X by LATTICE3:def 1 ;

for f being Function of (FixedUltraFilters X), the carrier of L

for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds

h = f -extension_to_hom

let L be non empty complete continuous Poset; :: thesis: for f being Function of (FixedUltraFilters X), the carrier of L

for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds

h = f -extension_to_hom

let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds

h = f -extension_to_hom

let h be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; :: thesis: ( h | (FixedUltraFilters X) = f implies h = f -extension_to_hom )

assume A1: h | (FixedUltraFilters X) = f ; :: thesis: h = f -extension_to_hom

set F = f -extension_to_hom ;

set cL = the carrier of L;

set BP = BoolePoset X;

set IP = InclPoset (Filt (BoolePoset X));

set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));

A2: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;

reconsider F9 = f -extension_to_hom as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;

reconsider h9 = h as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;

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: for Fi being Element of the carrier of (InclPoset (Filt (BoolePoset X))) holds h9 . Fi = F9 . Fi

hence
h = f -extension_to_hom
by FUNCT_2:63; :: thesis: verumset FUF = FixedUltraFilters X;

let Fi be Element of the carrier of (InclPoset (Filt (BoolePoset X))); :: thesis: h9 . Fi = F9 . Fi

Fi in Filt (BoolePoset X) by A2;

then consider FF being Filter of (BoolePoset X) such that

A4: Fi = FF ;

set Xsf = { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } ;

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

A5: { ("/\" ( { (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 FF } c= the carrier of (InclPoset (Filt (BoolePoset X)))

( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A5;

A7: ex_sup_of Xs, InclPoset (Filt (BoolePoset X)) by YELLOW_0:17;

A8: Xs is directed

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } by TARSKI:2;

A53: FF = "\/" ( { ("/\" ( { (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 FF } ,(InclPoset (Filt (BoolePoset X)))) by Th11;

h is directed-sups-preserving by WAYBEL16:def 1;

then h preserves_sup_of Xs by A8;

hence h9 . Fi = sup (h .: Xs) by A4, A53, A7

.= F9 . Fi by A4, A52, Def3 ;

:: thesis: verum

end;let Fi be Element of the carrier of (InclPoset (Filt (BoolePoset X))); :: thesis: h9 . Fi = F9 . Fi

Fi in Filt (BoolePoset X) by A2;

then consider FF being Filter of (BoolePoset X) such that

A4: Fi = FF ;

set Xsf = { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } ;

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

A5: { ("/\" ( { (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 FF } 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 FF } 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 FF } ; :: 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 FF ) ;

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 FF } 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 FF } ; :: 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 FF ) ;

hence p in the carrier of (InclPoset (Filt (BoolePoset X))) ; :: thesis: verum

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 FF } is empty

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 FF } is empty

consider YY being object such that

A6: YY in FF 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 FF } by A3, A6;

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 FF } is empty ; :: thesis: verum

end;A6: YY in FF 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 FF } by A3, A6;

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 FF } is empty ; :: thesis: verum

( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A5;

A7: ex_sup_of Xs, InclPoset (Filt (BoolePoset X)) by YELLOW_0:17;

A8: Xs is directed

proof

A31:
h is infs-preserving
by WAYBEL16:def 1;
let a, b be Element of (InclPoset (Filt (BoolePoset X))); :: according to WAYBEL_0:def 1 :: thesis: ( not a in Xs or not b in Xs or ex b_{1} being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st

( b_{1} in Xs & a <= b_{1} & b <= b_{1} ) )

assume that

A9: a in Xs and

A10: b in Xs ; :: thesis: ex b_{1} being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st

( b_{1} in Xs & a <= b_{1} & b <= b_{1} )

consider Yb being Subset of X such that

A11: b = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yb ) } ,(InclPoset (Filt (BoolePoset X)))) and

A12: Yb in FF by A10;

reconsider Yb9 = Yb as Element of FF by A12;

set Xsb = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yb ) } ;

consider Ya being Subset of X such that

A13: a = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Ya ) } ,(InclPoset (Filt (BoolePoset X)))) and

A14: Ya in FF by A9;

reconsider Ya9 = Ya as Element of FF by A14;

set Xsa = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Ya ) } ;

end;( b

assume that

A9: a in Xs and

A10: b in Xs ; :: thesis: ex b

( b

consider Yb being Subset of X such that

A11: b = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yb ) } ,(InclPoset (Filt (BoolePoset X)))) and

A12: Yb in FF by A10;

reconsider Yb9 = Yb as Element of FF by A12;

set Xsb = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yb ) } ;

consider Ya being Subset of X such that

A13: a = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Ya ) } ,(InclPoset (Filt (BoolePoset X)))) and

A14: Ya in FF by A9;

reconsider Ya9 = Ya as Element of FF by A14;

set Xsa = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Ya ) } ;

per cases
( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

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

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

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

( x = {z} & z in Yb ) } is empty ) ) ;

end;

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

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

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

( x = {z} & z in Yb ) } is empty ) ) ;

suppose A15:
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Ya ) } is empty ; :: thesis: ex b_{1} being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st

( b_{1} in Xs & a <= b_{1} & b <= b_{1} )

( x = {z} & z in Ya ) } is empty ; :: thesis: ex b

( b

take
a
; :: thesis: ( a in Xs & a <= a & b <= a )

thus a in Xs by A9; :: thesis: ( a <= a & b <= a )

thus a <= a ; :: thesis: b <= a

"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Ya ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A15;

hence b <= a by A13, YELLOW_0:45; :: thesis: verum

end;thus a in Xs by A9; :: thesis: ( a <= a & b <= a )

thus a <= a ; :: thesis: b <= a

"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Ya ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A15;

hence b <= a by A13, YELLOW_0:45; :: thesis: verum

suppose A16:
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yb ) } is empty ; :: thesis: ex b_{1} being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st

( b_{1} in Xs & a <= b_{1} & b <= b_{1} )

( x = {z} & z in Yb ) } is empty ; :: thesis: ex b

( b

take
b
; :: thesis: ( b in Xs & a <= b & b <= b )

thus b in Xs by A10; :: thesis: ( a <= b & b <= b )

"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yb ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A16;

hence a <= b by A11, YELLOW_0:45; :: thesis: b <= b

thus b <= b ; :: thesis: verum

end;thus b in Xs by A10; :: thesis: ( a <= b & b <= b )

"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yb ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A16;

hence a <= b by A11, YELLOW_0:45; :: thesis: b <= b

thus b <= b ; :: thesis: verum

suppose A17:
( not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

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

( x = {z} & z in Yb ) } is empty ) ; :: thesis: ex b_{1} being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st

( b_{1} in Xs & a <= b_{1} & b <= b_{1} )

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

( x = {z} & z in Yb ) } is empty ) ; :: thesis: ex b

( b

{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

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

( x = {z} & z in Yb ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A17;

{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

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

( x = {z} & z in Ya ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A17;

A18: "/\" (Xsb,(InclPoset (Filt (BoolePoset X)))) = meet Xsb by WAYBEL16:10;

consider Yab being Element of (BoolePoset X) such that

A19: Yab in FF and

A20: Yab <= Ya9 and

A21: Yab <= Yb9 by WAYBEL_0:def 2;

reconsider Yab = Yab as Element of FF by A19;

set c = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))));

set Xsc = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ;

A22: "/\" (Xsa,(InclPoset (Filt (BoolePoset X)))) = meet Xsa by WAYBEL16:10;

thus ex b_{1} being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st

( b_{1} in Xs & a <= b_{1} & b <= b_{1} )
:: thesis: verum

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

proof

then reconsider Xsb = { (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 Yb ) } 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 Yb ) } ; :: 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 Yb ) ) ;

hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; :: thesis: verum

end;( x = {z} & z in Yb ) } 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 Yb ) } ; :: 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 Yb ) ) ;

hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; :: thesis: verum

( x = {z} & z in Yb ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A17;

{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

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

proof

then reconsider Xsa = { (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 Ya ) } 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 Ya ) } ; :: 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 Ya ) ) ;

hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; :: thesis: verum

end;( x = {z} & z in Ya ) } 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 Ya ) } ; :: 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 Ya ) ) ;

hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; :: thesis: verum

( x = {z} & z in Ya ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A17;

A18: "/\" (Xsb,(InclPoset (Filt (BoolePoset X)))) = meet Xsb by WAYBEL16:10;

consider Yab being Element of (BoolePoset X) such that

A19: Yab in FF and

A20: Yab <= Ya9 and

A21: Yab <= Yb9 by WAYBEL_0:def 2;

reconsider Yab = Yab as Element of FF by A19;

set c = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))));

set Xsc = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ;

A22: "/\" (Xsa,(InclPoset (Filt (BoolePoset X)))) = meet Xsa by WAYBEL16:10;

thus ex b

( b

proof
end;

per cases
( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

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

( x = {z} & z in Yab ) } is empty ) ;

end;

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

( x = {z} & z in Yab ) } is empty ) ;

suppose A23:
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } is empty ; :: thesis: ex b_{1} being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st

( b_{1} in Xs & a <= b_{1} & b <= b_{1} )

( x = {z} & z in Yab ) } is empty ; :: thesis: ex b

( b

take
"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) ; :: thesis: ( "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs & a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

thus "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs by A3; :: thesis: ( a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

A24: "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A23;

hence a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_0:45; :: thesis: b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

thus b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by A24, YELLOW_0:45; :: thesis: verum

end;( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) ; :: thesis: ( "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs & a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

thus "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs by A3; :: thesis: ( a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

A24: "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A23;

hence a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_0:45; :: thesis: b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

thus b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by A24, YELLOW_0:45; :: thesis: verum

suppose A25:
not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } is empty ; :: thesis: ex b_{1} being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st

( b_{1} in Xs & a <= b_{1} & b <= b_{1} )

( x = {z} & z in Yab ) } is empty ; :: thesis: ex b

( b

{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

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

( x = {z} & z in Yab ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A25;

take "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) ; :: thesis: ( "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs & a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

thus "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs by A3; :: thesis: ( a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

A26: "/\" (Xsc,(InclPoset (Filt (BoolePoset X)))) = meet Xsc by WAYBEL16:10;

a c= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3; :: thesis: b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

b c= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3; :: thesis: verum

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

proof

then reconsider Xsc = { (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 Yab ) } 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 Yab ) } ; :: 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 Yab ) ) ;

hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; :: thesis: verum

end;( x = {z} & z in Yab ) } 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 Yab ) } ; :: 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 Yab ) ) ;

hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; :: thesis: verum

( x = {z} & z in Yab ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A25;

take "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) ; :: thesis: ( "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs & a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

thus "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs by A3; :: thesis: ( a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

A26: "/\" (Xsc,(InclPoset (Filt (BoolePoset X)))) = meet Xsc by WAYBEL16:10;

a c= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

proof

hence
a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in a or d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

Xsc c= Xsa

assume d in a ; :: thesis: d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

hence d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by A13, A22, A26, A28; :: thesis: verum

end;( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

Xsc c= Xsa

proof

then A28:
meet Xsa c= meet Xsc
by SETFAM_1:6;
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in Xsc or r in Xsa )

assume r in Xsc ; :: thesis: r in Xsa

then A27: ex xz being Element of (BoolePoset X) st

( r = uparrow xz & ex z being Element of X st

( xz = {z} & z in Yab ) ) ;

Yab c= Ya by A20, YELLOW_1:2;

hence r in Xsa by A27; :: thesis: verum

end;assume r in Xsc ; :: thesis: r in Xsa

then A27: ex xz being Element of (BoolePoset X) st

( r = uparrow xz & ex z being Element of X st

( xz = {z} & z in Yab ) ) ;

Yab c= Ya by A20, YELLOW_1:2;

hence r in Xsa by A27; :: thesis: verum

assume d in a ; :: thesis: d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

hence d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by A13, A22, A26, A28; :: thesis: verum

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3; :: thesis: b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

b c= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

proof

hence
b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in b or d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

Xsc c= Xsb

assume d in b ; :: thesis: d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

hence d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by A11, A18, A26, A30; :: thesis: verum

end;( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )

Xsc c= Xsb

proof

then A30:
meet Xsb c= meet Xsc
by SETFAM_1:6;
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in Xsc or r in Xsb )

assume r in Xsc ; :: thesis: r in Xsb

then A29: ex xz being Element of (BoolePoset X) st

( r = uparrow xz & ex z being Element of X st

( xz = {z} & z in Yab ) ) ;

Yab c= Yb by A21, YELLOW_1:2;

hence r in Xsb by A29; :: thesis: verum

end;assume r in Xsc ; :: thesis: r in Xsb

then A29: ex xz being Element of (BoolePoset X) st

( r = uparrow xz & ex z being Element of X st

( xz = {z} & z in Yab ) ) ;

Yab c= Yb by A21, YELLOW_1:2;

hence r in Xsb by A29; :: thesis: verum

assume d in b ; :: thesis: d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))

hence d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by A11, A18, A26, A30; :: thesis: verum

( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3; :: thesis: verum

now :: thesis: for s being object holds

( ( s in h .: Xs implies s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } ) & ( s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } implies s in h .: Xs ) )

then A52:
h .: Xs = { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( ( s in h .: Xs implies s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } ) & ( s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } implies s in h .: Xs ) )

let s be object ; :: thesis: ( ( s in h .: Xs implies s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } ) & ( s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } implies s in h .: Xs ) )

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } ; :: thesis: s in h .: Xs

then consider Y being Subset of X such that

A42: s = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L) and

A43: Y in FF ;

set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

{ (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 Subset of (InclPoset (Filt (BoolePoset X))) ;

set Xsif = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

( h preserves_inf_of Xsi & ex_inf_of Xsi, InclPoset (Filt (BoolePoset X)) ) by A31, YELLOW_0:17;

then A44: inf (h .: Xsi) = h . (inf Xsi) ;

( x = {z} & z in Y ) } by TARSKI:2;

inf Xsi in Xs by A43;

hence s in h .: Xs by A42, A44, A51, FUNCT_2:35; :: thesis: verum

end;( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } ) & ( s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } implies s in h .: Xs ) )

hereby :: thesis: ( s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } implies s in h .: Xs )

assume
s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } implies s in h .: Xs )

assume
s in h .: Xs
; :: thesis: s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF }

then consider t being object such that

t in the carrier of (InclPoset (Filt (BoolePoset X))) and

A32: t in Xs and

A33: s = h . t by FUNCT_2:64;

consider Y being Subset of X such that

A34: ( t = "/\" ( { (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)))) & Y in FF ) by A32;

set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

{ (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 Subset of (InclPoset (Filt (BoolePoset X))) ;

set Xsif = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

( x = {z} & z in Y ) } by TARSKI:2;

( h preserves_inf_of Xsi & ex_inf_of Xsi, InclPoset (Filt (BoolePoset X)) ) by A31, YELLOW_0:17;

then inf (h .: Xsi) = h . (inf Xsi) ;

hence s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } by A33, A34, A41; :: thesis: verum

end;( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF }

then consider t being object such that

t in the carrier of (InclPoset (Filt (BoolePoset X))) and

A32: t in Xs and

A33: s = h . t by FUNCT_2:64;

consider Y being Subset of X such that

A34: ( t = "/\" ( { (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)))) & Y in FF ) by A32;

set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

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

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 A2; :: 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 A2; :: thesis: verum

( x = {z} & z in Y ) } as Subset of (InclPoset (Filt (BoolePoset X))) ;

set Xsif = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

now :: thesis: for u being object holds

( ( u in h .: Xsi implies u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi ) )

then A41:
h .: Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( ( u in h .: Xsi implies u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi ) )

let u be object ; :: thesis: ( ( u in h .: Xsi implies u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi ) )

( x = {z} & z in Y ) } ; :: thesis: u in h .: Xsi

then consider x being Element of (BoolePoset X) such that

A38: u = f . (uparrow x) and

A39: ex z being Element of X st

( x = {z} & z in Y ) ;

uparrow x in FixedUltraFilters X by A39;

then A40: h . (uparrow x) = f . (uparrow x) by A1, FUNCT_1:49;

uparrow x in Xsi by A39;

hence u in h .: Xsi by A38, A40, FUNCT_2:35; :: thesis: verum

end;( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi ) )

hereby :: thesis: ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi )

assume
u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( x = {z} & z in Y ) } implies u in h .: Xsi )

assume
u in h .: Xsi
; :: thesis: u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) }

then consider v being object such that

v in the carrier of (InclPoset (Filt (BoolePoset X))) and

A35: v in Xsi and

A36: u = h . v by FUNCT_2:64;

A37: ex x being Element of (BoolePoset X) st

( v = uparrow x & ex z being Element of X st

( x = {z} & z in Y ) ) by A35;

then v in FixedUltraFilters X ;

then h . v = f . v by A1, FUNCT_1:49;

hence u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } by A36, A37; :: thesis: verum

end;( x = {z} & z in Y ) }

then consider v being object such that

v in the carrier of (InclPoset (Filt (BoolePoset X))) and

A35: v in Xsi and

A36: u = h . v by FUNCT_2:64;

A37: ex x being Element of (BoolePoset X) st

( v = uparrow x & ex z being Element of X st

( x = {z} & z in Y ) ) by A35;

then v in FixedUltraFilters X ;

then h . v = f . v by A1, FUNCT_1:49;

hence u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } by A36, A37; :: thesis: verum

( x = {z} & z in Y ) } ; :: thesis: u in h .: Xsi

then consider x being Element of (BoolePoset X) such that

A38: u = f . (uparrow x) and

A39: ex z being Element of X st

( x = {z} & z in Y ) ;

uparrow x in FixedUltraFilters X by A39;

then A40: h . (uparrow x) = f . (uparrow x) by A1, FUNCT_1:49;

uparrow x in Xsi by A39;

hence u in h .: Xsi by A38, A40, FUNCT_2:35; :: thesis: verum

( x = {z} & z in Y ) } by TARSKI:2;

( h preserves_inf_of Xsi & ex_inf_of Xsi, InclPoset (Filt (BoolePoset X)) ) by A31, YELLOW_0:17;

then inf (h .: Xsi) = h . (inf Xsi) ;

hence s in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } by A33, A34, A41; :: thesis: verum

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } ; :: thesis: s in h .: Xs

then consider Y being Subset of X such that

A42: s = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L) and

A43: Y in FF ;

set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

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

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 A2; :: 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 A2; :: thesis: verum

( x = {z} & z in Y ) } as Subset of (InclPoset (Filt (BoolePoset X))) ;

set Xsif = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

( h preserves_inf_of Xsi & ex_inf_of Xsi, InclPoset (Filt (BoolePoset X)) ) by A31, YELLOW_0:17;

then A44: inf (h .: Xsi) = h . (inf Xsi) ;

now :: thesis: for u being object holds

( ( u in h .: Xsi implies u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi ) )

then A51:
h .: Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( ( u in h .: Xsi implies u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi ) )

let u be object ; :: thesis: ( ( u in h .: Xsi implies u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi ) )

( x = {z} & z in Y ) } ; :: thesis: u in h .: Xsi

then consider x being Element of (BoolePoset X) such that

A48: u = f . (uparrow x) and

A49: ex z being Element of X st

( x = {z} & z in Y ) ;

uparrow x in FixedUltraFilters X by A49;

then A50: h . (uparrow x) = f . (uparrow x) by A1, FUNCT_1:49;

uparrow x in Xsi by A49;

hence u in h .: Xsi by A48, A50, FUNCT_2:35; :: thesis: verum

end;( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi ) )

hereby :: thesis: ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies u in h .: Xsi )

assume
u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( x = {z} & z in Y ) } implies u in h .: Xsi )

assume
u in h .: Xsi
; :: thesis: u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) }

then consider v being object such that

v in the carrier of (InclPoset (Filt (BoolePoset X))) and

A45: v in Xsi and

A46: u = h . v by FUNCT_2:64;

A47: ex x being Element of (BoolePoset X) st

( v = uparrow x & ex z being Element of X st

( x = {z} & z in Y ) ) by A45;

then v in FixedUltraFilters X ;

then h . v = f . v by A1, FUNCT_1:49;

hence u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } by A46, A47; :: thesis: verum

end;( x = {z} & z in Y ) }

then consider v being object such that

v in the carrier of (InclPoset (Filt (BoolePoset X))) and

A45: v in Xsi and

A46: u = h . v by FUNCT_2:64;

A47: ex x being Element of (BoolePoset X) st

( v = uparrow x & ex z being Element of X st

( x = {z} & z in Y ) ) by A45;

then v in FixedUltraFilters X ;

then h . v = f . v by A1, FUNCT_1:49;

hence u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } by A46, A47; :: thesis: verum

( x = {z} & z in Y ) } ; :: thesis: u in h .: Xsi

then consider x being Element of (BoolePoset X) such that

A48: u = f . (uparrow x) and

A49: ex z being Element of X st

( x = {z} & z in Y ) ;

uparrow x in FixedUltraFilters X by A49;

then A50: h . (uparrow x) = f . (uparrow x) by A1, FUNCT_1:49;

uparrow x in Xsi by A49;

hence u in h .: Xsi by A48, A50, FUNCT_2:35; :: thesis: verum

( x = {z} & z in Y ) } by TARSKI:2;

inf Xsi in Xs by A43;

hence s in h .: Xs by A42, A44, A51, FUNCT_2:35; :: thesis: verum

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in FF } by TARSKI:2;

A53: FF = "\/" ( { ("/\" ( { (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 FF } ,(InclPoset (Filt (BoolePoset X)))) by Th11;

h is directed-sups-preserving by WAYBEL16:def 1;

then h preserves_sup_of Xs by A8;

hence h9 . Fi = sup (h .: Xs) by A4, A53, A7

.= F9 . Fi by A4, A52, Def3 ;

:: thesis: verum