set FUF = FixedUltraFilters X;
set cL = the carrier of L;
set F = f -extension_to_hom ;
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;
let Fs be Subset of (InclPoset (Filt (BoolePoset X))); :: according to WAYBEL_0:def 32 :: thesis:
assume ex_inf_of Fs, InclPoset (Filt (BoolePoset X)) ; :: according to WAYBEL_0:def 30 :: thesis:
thus ex_inf_of (f -extension_to_hom) .: Fs,L by YELLOW_0:17; :: thesis:
A2: BoolePoset X = InclPoset (bool X) by YELLOW_1:4;
A3: InclPoset (bool X) = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def 1;
then A4: the carrier of (BoolePoset X) = bool X by YELLOW_1:4;

then ( "/\" (((f -extension_to_hom) .: Fs),L) = Top L & "/\" (Fs,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) ) ;
hence "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X))))) by Th13; :: thesis:

end;

suppose not Fs is empty ; :: thesis:

then reconsider Fs9 = Fs as non empty Subset of (InclPoset (Filt (BoolePoset X))) ;
defpred S₁[ object , object , object ] means ex D2 being set st
( D2 = L & X = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in D2 ) } ,L) );
deffunc H₁( Element of Fs9) -> set = { ("/\" ( { (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 X } ;
not {} in Fs9 ;
then Fs9 is with_non-empty_elements by SETFAM_1:def 8;
then reconsider K = id Fs9 as V8() ManySortedSet of Fs9 ;
A5: for i being object st i in Fs9 holds
for s being object st s in K . i holds
ex y being object st
( y in (Fs9 --> the carrier of L) . i & S₁[y,s,i] )

proof

let i be object ; :: thesis:
assume A6: i in Fs9 ; :: thesis:
let s be object ; :: thesis:
assume s in K . i ; :: thesis:
reconsider D2 = s as set by TARSKI:1;
take y = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in D2 ) } ,L); :: thesis:
y in the carrier of L ;
hence y in (Fs9 --> the carrier of L) . i by A6, FUNCOP_1:7; :: thesis:
take D2 ; :: thesis:
thus D2 = s ; :: thesis:
thus y = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in D2 ) } ,L) ; :: thesis:

end;

consider FD being ManySortedFunction of K,Fs9 --> the carrier of L such that
A7: for i being object st i in Fs9 holds
ex g being Function of (K . i),((Fs9 --> the carrier of L) . i) st
( g = FD . i & ( for s being object st s in K . i holds
S₁[g . s,s,i] ) ) from MSSUBFAM:sch 1(A5);
defpred S₂[ Element of Fs9] means rng (FD . X) = H₁(X);
A8: for s being Element of Fs9 holds S₂[s]

proof

let s be Element of Fs9; :: thesis:

now :: thesis:

let t be object ; :: thesis:
consider g being Function of (K . s),((Fs9 --> the carrier of L) . s) such that
A9: g = FD . s and
A10: for u being object st u in K . s holds
S₁[g . u,u,s] by A7;

hereby :: thesis:

assume t in rng (FD . s) ; :: thesis:
then consider u being object such that
A11: u in dom (FD . s) and
A12: t = (FD . s) . u by FUNCT_1:def 3;
consider g being Function of (K . s),((Fs9 --> the carrier of L) . s) such that
A13: g = FD . s and
A14: for u being object st u in K . s holds
S₁[g . u,u,s] by A7;
A15: dom (FD . s) = K . s by FUNCT_2:def 1;
reconsider u = u as set by TARSKI:1;
S₁[g . u,u,s] by A11, A14;
then A16: g . u = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in u ) } ,L) ;
s in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then ( K . s = s & ex FF being Filter of (BoolePoset X) st s = FF ) by A1;
then reconsider u = u as Subset of X by A3, A11, A15, YELLOW_1:4;
u in s by A11;
then t 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 s } by A12, A13, A16;
hence t in H₁(s) ; :: thesis:

end;

assume t in H₁(s) ; :: thesis:
then consider Y being Subset of X such that
A17: t = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) and
A18: Y in s ;
dom (FD . s) = K . s by FUNCT_2:def 1;
then A19: Y in dom (FD . s) by A18;
S₁[g . Y,Y,s] by A10, A18;
then g . Y = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) ;
hence t in rng (FD . s) by A17, A19, A9, FUNCT_1:def 3; :: thesis:

end;

hence S₂[s] by TARSKI:2; :: thesis:

end;

meet Fs9 is Filter of (BoolePoset X) by WAYBEL16:9;
then meet Fs9 in Filt (BoolePoset X) ;
then reconsider mFs = meet Fs9 as Element of the carrier of (InclPoset (Filt (BoolePoset X))) by A1;
set smFs = { ("/\" ( { (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 mFs } ;
A20: dom FD = Fs9 by PARTFUN1:def 2;
reconsider FD = FD as DoubleIndexedSet of K,L ;

now :: thesis:

let r be object ; :: thesis:

hereby :: thesis:

assume r in (f -extension_to_hom) .: Fs ; :: thesis:
then consider s being object such that
A21: s in the carrier of (InclPoset (Filt (BoolePoset X))) and
A22: s in Fs and
A23: (f -extension_to_hom) . s = r by FUNCT_2:64;
reconsider s9 = s as Element of the carrier of (InclPoset (Filt (BoolePoset X))) by A21;
reconsider s = s as Element of Fs9 by A22;
A24: S₂[s] by A8;
(f -extension_to_hom) . s9 = "\/" ( { ("/\" ( { (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 s9 } ,L) by Def3;
then r = Sup by A23, A24, YELLOW_2:def 5;
hence r in rng (Sups ) by WAYBEL_5:14; :: thesis:

end;

assume r in rng (Sups ) ; :: thesis:
then consider s being Element of Fs9 such that
A25: r = Sup by WAYBEL_5:14;
S₂[s] by A8;
then (f -extension_to_hom) . s = "\/" ((rng (FD . s)),L) by Def3
.= Sup by YELLOW_2:def 5 ;
hence r in (f -extension_to_hom) .: Fs by A25, FUNCT_2:35; :: thesis:

end;

then (f -extension_to_hom) .: Fs = rng (Sups ) by TARSKI:2;
then A26: inf ((f -extension_to_hom) .: Fs) = Inf by YELLOW_2:def 6;

A27: now :: thesis:

reconsider pdFD = product (doms FD) as non empty functional set ;
let r be object ; :: thesis:
reconsider dFFD = (product (doms FD)) --> Fs9 as ManySortedSet of pdFD ;
reconsider FFD = Frege FD as DoubleIndexedSet of dFFD,L ;
deffunc H₂( Element of pdFD) -> set = { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in X . u ) } ,L)) where u is Element of Fs9 : u in dom (FFD . X) } ;
A28: dom FFD = pdFD by PARTFUN1:def 2;

A29: now :: thesis:

let s be Element of pdFD; :: thesis:
A30: dom FD = dom (FFD . s) by A28, WAYBEL_5:8;

now :: thesis:

let t be object ; :: thesis:

hereby :: thesis:

assume t in rng (FFD . s) ; :: thesis:
then consider u being object such that
A31: u in dom (FFD . s) and
A32: t = (FFD . s) . u by FUNCT_1:def 3;
A33: (FFD . s) . u = (FD . u) . (s . u) by A28, A30, A31, WAYBEL_5:9;
reconsider u = u as Element of Fs9 by A31;
consider g being Function of (K . u),((Fs9 --> the carrier of L) . u) such that
A34: g = FD . u and
A35: for v being object st v in K . u holds
S₁[g . v,v,u] by A7;
dom (FD . u) = K . u by FUNCT_2:def 1;
then S₁[g . (s . u),s . u,s] by A20, A28, A35, WAYBEL_5:9;
then g . (s . u) = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,L) ;
hence t in H₂(s) by A31, A32, A33, A34; :: thesis:

end;

assume t in H₂(s) ; :: thesis:
then consider u being Element of Fs9 such that
A36: ( t = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,L) & u in dom (FFD . s) ) ;
reconsider u = u as Element of Fs9 ;
consider g being Function of (K . u),((Fs9 --> the carrier of L) . u) such that
A37: g = FD . u and
A38: for v being object st v in K . u holds
S₁[g . v,v,u] by A7;
dom (FD . u) = K . u by FUNCT_2:def 1;
then S₁[g . (s . u),s . u,s] by A20, A28, A38, WAYBEL_5:9;
then g . (s . u) = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,L) ;
hence t in rng (FFD . s) by A28, A30, A36, A37, WAYBEL_5:9; :: thesis:

end;

hence rng (FFD . s) = H₂(s) by TARSKI:2; :: thesis:

end;

hereby :: thesis:

assume r in rng (Infs ) ; :: thesis:
then consider s being Element of pdFD such that
A39: r = Inf by WAYBEL_5:14;
set idFFDs = { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } ;
A40: { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } c= bool the carrier of L

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
reconsider tt = t as set by TARSKI:1;
assume t in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } ; :: thesis:
then consider u being Element of Fs9 such that
A41: t = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } and
u in dom (FFD . s) ;
tt c= the carrier of L

proof

let v be object ; :: according to TARSKI:def 3 :: thesis:
assume v in tt ; :: thesis:
then consider x being Element of (BoolePoset X) such that
A42: v = f . (uparrow x) and
A43: ex z being Element of X st
( x = {z} & z in s . u ) by A41;
uparrow x in FixedUltraFilters X by A43;
hence v in the carrier of L by A42, FUNCT_2:5; :: thesis:

end;

hence t in bool the carrier of L ; :: thesis:

end;

now :: thesis:

let t be object ; :: thesis:

hereby :: thesis:

assume t in H₂(s) ; :: thesis:
then consider u being Element of Fs9 such that
A44: t = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,L) and
A45: u in dom (FFD . s) ;
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } c= the carrier of L

proof

let v be object ; :: according to TARSKI:def 3 :: thesis:
assume v in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ; :: thesis:
then consider x being Element of (BoolePoset X) such that
A46: v = f . (uparrow x) and
A47: ex z being Element of X st
( x = {z} & z in s . u ) ;
uparrow x in FixedUltraFilters X by A47;
hence v in the carrier of L by A46, FUNCT_2:5; :: thesis:

end;

then reconsider Y1 = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } as Subset of L ;
Y1 in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } by A45;
hence t in { (inf YY) where YY is Subset of L : YY in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } } by A44; :: thesis:

end;

assume t in { (inf YY) where YY is Subset of L : YY in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } } ; :: thesis:
then consider YY being Subset of L such that
A48: t = inf YY and
A49: YY in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } ;
ex u1 being Element of Fs9 st
( YY = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u1 ) } & u1 in dom (FFD . s) ) by A49;
hence t in H₂(s) by A48; :: thesis:

end;

then A50: H₂(s) = { (inf YY) where YY is Subset of L : YY in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } } by TARSKI:2;
A51: dom s = dom FD by A28, WAYBEL_5:8;
union (rng s) c= X

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in union (rng s) ; :: thesis:
then consider te being set such that
A52: t in te and
A53: te in rng s by TARSKI:def 4;
consider u being object such that
A54: u in dom s and
A55: te = s . u by A53, FUNCT_1:def 3;
reconsider u = u as set by TARSKI:1;
FD . u is Function of (K . u), the carrier of L by A51, A54, WAYBEL_5:6;
then dom (FD . u) = K . u by FUNCT_2:def 1
.= u by A51, A54, FUNCT_1:17 ;
then A56: te in u by A28, A51, A54, A55, WAYBEL_5:9;
u in the carrier of (InclPoset (Filt (BoolePoset X))) by A20, A51, A54;
then ex FF being Filter of (BoolePoset X) st u = FF by A1;
hence t in X by A4, A52, A56; :: thesis:

end;

then reconsider Y = union (rng s) as Subset of X ;
set Ys = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
A57: dom FD = dom (FFD . s) by A28, WAYBEL_5:8;

now :: thesis:

let t be object ; :: thesis:

hereby :: thesis:

assume t in union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } ; :: thesis:
then consider te being set such that
A58: t in te and
A59: te in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } by TARSKI:def 4;
consider u being Element of Fs9 such that
A60: te = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } and
A61: u in dom (FFD . s) by A59;
consider x being Element of (BoolePoset X) such that
A62: t = f . (uparrow x) and
A63: ex z being Element of X st
( x = {z} & z in s . u ) by A58, A60;
consider z being Element of X such that
A64: x = {z} and
A65: z in s . u by A63;
s . u in rng s by A57, A51, A61, FUNCT_1:def 3;
then z in Y by A65, TARSKI:def 4;
hence t in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by A62, A64; :: thesis:

end;

assume t 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
A66: t = f . (uparrow x) and
A67: ex z being Element of X st
( x = {z} & z in Y ) ;
consider z being Element of X such that
A68: x = {z} and
A69: z in Y by A67;
consider ze being set such that
A70: z in ze and
A71: ze in rng s by A69, TARSKI:def 4;
consider u being object such that
A72: u in dom s and
A73: ze = s . u by A71, FUNCT_1:def 3;
reconsider u = u as Element of Fs9 by A51, A72;
A74: { (f . (uparrow x1)) where x1 is Element of (BoolePoset X) : ex z being Element of X st
( x1 = {z} & z in s . u ) } in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } by A57, A51, A72;
t in { (f . (uparrow x1)) where x1 is Element of (BoolePoset X) : ex z being Element of X st
( x1 = {z} & z in s . u ) } by A66, A68, A70, A73;
hence t in union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } by A74, TARSKI:def 4; :: thesis:

end;

then A75: union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } = { (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;

now :: thesis:

reconsider Y9 = Y as Element of (BoolePoset X) by A3, YELLOW_1:4;
let Z be set ; :: thesis:
assume A76: Z in Fs9 ; :: thesis:
then FD . Z is Function of (K . Z), the carrier of L by WAYBEL_5:6;
then A77: dom (FD . Z) = K . Z by FUNCT_2:def 1
.= Z by A76, FUNCT_1:17 ;
s . Z in rng s by A20, A51, A76, FUNCT_1:def 3;
then A78: s . Z c= Y by ZFMISC_1:74;
then reconsider sZ = s . Z as Element of (BoolePoset X) by A2, A3, XBOOLE_1:1;
A79: sZ <= Y9 by A78, YELLOW_1:2;
Z in the carrier of (InclPoset (Filt (BoolePoset X))) by A76;
then A80: ex FF being Filter of (BoolePoset X) st Z = FF by A1;
s . Z in dom (FD . Z) by A20, A28, A76, WAYBEL_5:9;
hence Y in Z by A80, A77, A79, WAYBEL_0:def 20; :: thesis:

end;

then Y in mFs by SETFAM_1:def 1;
then A81: "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) 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 mFs } ;
"/\" ((rng (FFD . s)),L) = "/\" (H₂(s),L) by A29
.= "/\" ((union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } ),L) by A40, A50, Lm1 ;
hence r 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 mFs } by A39, A81, A75, YELLOW_2:def 6; :: thesis:

end;

assume r 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 mFs } ; :: thesis:
then consider Y being Subset of X such that
A82: r = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) and
A83: Y in mFs ;
A84: "/\" ({r},L) = r by A82, YELLOW_0:39;
set s = Fs9 --> Y;
A85: dom (doms FD) = dom FD by FUNCT_6:59
.= dom (Fs9 --> Y) by A20 ;

A86: now :: thesis:

let w be object ; :: thesis:
assume A87: w in dom (doms FD) ; :: thesis:
then FD . w is Function of (K . w),((Fs9 --> the carrier of L) . w) by A85, PBOOLE:def 15;
then A88: dom (FD . w) = K . w by A85, A87, FUNCT_2:def 1
.= w by A85, A87, FUNCT_1:18 ;
( (doms FD) . w = dom (FD . w) & (Fs9 --> Y) . w = Y ) by A20, A85, A87, FUNCOP_1:7, FUNCT_6:22;
hence (Fs9 --> Y) . w in (doms FD) . w by A83, A85, A87, A88, SETFAM_1:def 1; :: thesis:

end;

set s9 = Fs9 --> Y;
reconsider s = Fs9 --> Y as Element of pdFD by A85, A86, CARD_3:9;

now :: thesis:

set u = the Element of Fs9;
let t be object ; :: thesis:
A89: ( dom (Fs9 --> Y) = Fs9 & s . the Element of Fs9 = Y ) ;

hereby :: thesis:

assume t in H₂(s) ; :: thesis:
then consider u being Element of Fs9 such that
A90: t = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,L) and
u in dom (FFD . s) ;
thus t in {r} by A82, A90, TARSKI:def 1; :: thesis:

end;

assume t in {r} ; :: thesis:
then A91: t = r by TARSKI:def 1;
( dom FD = dom (FFD . s) & dom s = dom FD ) by A28, WAYBEL_5:8;
hence t in H₂(s) by A82, A91, A89; :: thesis:

end;

then A92: { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,L)) where u is Element of Fs9 : u in dom (FFD . s) } = {r} by TARSKI:2;
( Inf = "/\" ((rng (FFD . s)),L) & rng (FFD . s) = H₂(s) ) by A29, YELLOW_2:def 6;
hence r in rng (Infs ) by A92, A84, WAYBEL_5:14; :: thesis:

end;

for j being Element of Fs9 holds rng (FD . j) is directed

proof

let j be Element of Fs9; :: thesis:
let k, m be Element of L; :: according to WAYBEL_0:def 1 :: thesis:
assume that
A93: k in rng (FD . j) and
A94: m in rng (FD . j) ; :: thesis:
consider kd being object such that
A95: kd in dom (FD . j) and
A96: (FD . j) . kd = k by A93, FUNCT_1:def 3;
consider md being object such that
A97: md in dom (FD . j) and
A98: (FD . j) . md = m by A94, FUNCT_1:def 3;
j in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then consider FF being Filter of (BoolePoset X) such that
A99: j = FF by A1;
A100: dom (FD . j) = K . j by FUNCT_2:def 1;
then reconsider kd = kd as Element of (BoolePoset X) by A95, A99;
reconsider md = md as Element of (BoolePoset X) by A97, A100, A99;
consider nd being Element of (BoolePoset X) such that
A101: nd in FF and
A102: nd <= kd and
A103: nd <= md by A95, A97, A99, WAYBEL_0:def 2;
set n = (FD . j) . nd;
A104: (FD . j) . nd in rng (FD . j) by A100, A99, A101, FUNCT_1:def 3;
consider g being Function of (K . j),((Fs9 --> the carrier of L) . j) such that
A105: g = FD . j and
A106: for u being object st u in K . j holds
S₁[g . u,u,j] by A7;
set nds = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ;
S₁[g . nd,nd,j] by A99, A101, A106;
then A107: g . nd = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ,L) ;
reconsider n = (FD . j) . nd as Element of L by A104;
take n ; :: thesis:
thus n in rng (FD . j) by A100, A99, A101, FUNCT_1:def 3; :: thesis:
A108: ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ,L by YELLOW_0:17;
set mds = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } ;
A109: nd c= md by A103, YELLOW_1:2;
A110: { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } c= { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) }

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ; :: thesis:
then ex x being Element of (BoolePoset X) st
( w = f . (uparrow x) & ex z being Element of X st
( x = {z} & z in nd ) ) ;
hence w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } by A109; :: thesis:

end;

A111: ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } ,L by YELLOW_0:17;
set kds = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) } ;
A112: ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) } ,L by YELLOW_0:17;
A113: nd c= kd by A102, YELLOW_1:2;
A114: { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } c= { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) }

proof

end;

S₁[g . kd,kd,j] by A95, A106;
then g . kd = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) } ,L) ;
hence k <= n by A96, A105, A107, A112, A108, A114, YELLOW_0:35; :: thesis:
S₁[g . md,md,j] by A97, A106;
then g . md = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } ,L) ;
hence m <= n by A98, A105, A107, A108, A111, A110, YELLOW_0:35; :: thesis:

end;

then A115: Inf = Sup by WAYBEL_5:19
.= "\/" ((rng (Infs )),L) by YELLOW_2:def 5 ;
( inf Fs9 = meet Fs9 & (f -extension_to_hom) . (meet Fs9) = "\/" ( { ("/\" ( { (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 mFs } ,L) ) by Def3, WAYBEL16:10;
hence "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X))))) by A26, A115, A27, TARSKI:2; :: thesis:

end;