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 ;

now :: thesis: for Fi being Element of the carrier of (InclPoset (Filt (BoolePoset X))) holds h9 . Fi = F9 . Fi

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

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;

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

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;

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

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₁ being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b₁ in Xs & a <= b₁ & b <= b₁ ) )
assume that
A9: a in Xs and
A10: b in Xs ; :: thesis: ex b₁ being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b₁ in Xs & a <= b₁ & 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 ) ) ;

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₁ being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b₁ in Xs & a <= b₁ & 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;

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₁ being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b₁ in Xs & a <= b₁ & 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;

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₁ being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b₁ in Xs & 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 ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in 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;

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

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;

then reconsider Xsa = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( 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₁ being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b₁ in Xs & a <= b₁ & b <= b₁ ) :: thesis: verum

proof

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

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₁ being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b₁ in Xs & a <= b₁ & 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;

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₁ being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b₁ in Xs & a <= b₁ & 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)))

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in 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;

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

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

proof

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;

then A28: meet Xsa c= meet Xsc by SETFAM_1:6;
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;

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

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

proof

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;

then A30: meet Xsb c= meet Xsc by SETFAM_1:6;
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;

hence 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 YELLOW_1:3; :: thesis: verum

end;

end;

end;

end;

end;

end;

A31: h is infs-preserving by WAYBEL16:def 1;

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

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

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

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; :: thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; :: 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 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 ) )

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

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

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

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

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

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;

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

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

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

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

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

then A52: h .: Xs = { ("/\" ( { (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 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;

hence h = f -extension_to_hom by FUNCT_2:63; :: thesis: verum