let X be set ; :: thesis:
let L be non empty complete continuous Poset; :: thesis:
let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis:
let h be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; :: thesis:
assume A1: h | (FixedUltraFilters X) = f ; :: thesis:
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 ;

set FUF = FixedUltraFilters X;
let Fi be Element of the carrier of (InclPoset (Filt (BoolePoset X))); :: thesis:
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)))

let p be object ; :: according to TARSKI:def 3 :: thesis:
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:
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:

end;

now :: thesis:

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:

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:
assume that
A9: a in Xs and
A10: b in Xs ; :: thesis:
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 ) 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:

take a ; :: thesis:
thus a in Xs by A9; :: thesis:
thus a <= a ; :: thesis:
"/\" ( { (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:

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:

take b ; :: thesis:
thus b in Xs by A10; :: thesis:
"/\" ( { (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:
thus b <= b ; :: thesis:

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:

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

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

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:

proof

per cases ) 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:

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

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:

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

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:
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:
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:
Xsc c= Xsa

proof

let r be object ; :: according to TARSKI:def 3 :: thesis:
assume r in Xsc ; :: thesis:
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:

end;

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

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 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:
Xsc c= Xsb

proof

let r be object ; :: according to TARSKI:def 3 :: thesis:
assume r in Xsc ; :: thesis:
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:

end;

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

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:

end;

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

now :: thesis:

let s be object ; :: thesis:

hereby :: thesis:

assume s in h .: Xs ; :: thesis:
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:
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:
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:

end;

now :: thesis:

let u be object ; :: thesis:

hereby :: thesis:

assume u in h .: Xsi ; :: thesis:
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:

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

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:

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

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:

let u be object ; :: thesis:

hereby :: thesis:

assume u in h .: Xsi ; :: thesis:
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:

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

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:

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:

end;

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