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: f -extension_to_hom preserves_inf_of Fs

assume ex_inf_of Fs, InclPoset (Filt (BoolePoset X)) ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (f -extension_to_hom) .: Fs,L & "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X))))) )

thus ex_inf_of (f -extension_to_hom) .: Fs,L by YELLOW_0:17; :: thesis: "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X)))))

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;

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: f -extension_to_hom preserves_inf_of Fs

assume ex_inf_of Fs, InclPoset (Filt (BoolePoset X)) ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (f -extension_to_hom) .: Fs,L & "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X))))) )

thus ex_inf_of (f -extension_to_hom) .: Fs,L by YELLOW_0:17; :: thesis: "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X)))))

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;

per cases
( Fs is empty or not Fs is empty )
;

end;

suppose
Fs is empty
; :: thesis: "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X)))))

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

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

suppose
not Fs is empty
; :: thesis: "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X)))))

then reconsider Fs9 = Fs as non empty Subset of (InclPoset (Filt (BoolePoset X))) ;

defpred S_{1}[ 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_{1}( 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_{1}[y,s,i] )

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_{1}[g . s,s,i] ) )
from MSSUBFAM:sch 1(A5);

defpred S_{2}[ Element of Fs9] means rng (FD . X) = H_{1}(X);

A8: for s being Element of Fs9 holds S_{2}[s]

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 ;

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

.= "\/" ((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: verum

end;defpred S

( 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

( 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

proof

consider FD being ManySortedFunction of K,Fs9 --> the carrier of L such that
let i be object ; :: thesis: ( i in Fs9 implies for s being object st s in K . i holds

ex y being object st

( y in (Fs9 --> the carrier of L) . i & S_{1}[y,s,i] ) )

assume A6: i in Fs9 ; :: thesis: for s being object st s in K . i holds

ex y being object st

( y in (Fs9 --> the carrier of L) . i & S_{1}[y,s,i] )

let s be object ; :: thesis: ( s in K . i implies ex y being object st

( y in (Fs9 --> the carrier of L) . i & S_{1}[y,s,i] ) )

assume s in K . i ; :: thesis: ex y being object st

( y in (Fs9 --> the carrier of L) . i & S_{1}[y,s,i] )

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 (Fs9 --> the carrier of L) . i & S_{1}[y,s,i] )

y in the carrier of L ;

hence y in (Fs9 --> the carrier of L) . i by A6, FUNCOP_1:7; :: thesis: S_{1}[y,s,i]

take D2 ; :: thesis: ( D2 = s & y = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in D2 ) } ,L) )

thus D2 = s ; :: thesis: y = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in D2 ) } ,L)

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

end;ex y being object st

( y in (Fs9 --> the carrier of L) . i & S

assume A6: i in Fs9 ; :: thesis: for s being object st s in K . i holds

ex y being object st

( y in (Fs9 --> the carrier of L) . i & S

let s be object ; :: thesis: ( s in K . i implies ex y being object st

( y in (Fs9 --> the carrier of L) . i & S

assume s in K . i ; :: thesis: ex y being object st

( y in (Fs9 --> the carrier of L) . i & S

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 (Fs9 --> the carrier of L) . i & S

y in the carrier of L ;

hence y in (Fs9 --> the carrier of L) . i by A6, FUNCOP_1:7; :: thesis: S

take D2 ; :: thesis: ( D2 = s & y = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in D2 ) } ,L) )

thus D2 = s ; :: thesis: y = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in D2 ) } ,L)

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

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

defpred S

A8: for s being Element of Fs9 holds S

proof

meet Fs9 is Filter of (BoolePoset X)
by WAYBEL16:9;
let s be Element of Fs9; :: thesis: S_{2}[s]

_{2}[s]
by TARSKI:2; :: thesis: verum

end;now :: thesis: for t being object holds

( ( t in rng (FD . s) implies t in H_{1}(s) ) & ( t in H_{1}(s) implies t in rng (FD . s) ) )

hence
S( ( t in rng (FD . s) implies t in H

let t be object ; :: thesis: ( ( t in rng (FD . s) implies t in H_{1}(s) ) & ( t in H_{1}(s) implies t in rng (FD . s) ) )

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_{1}[g . u,u,s]
by A7;

_{1}(s)
; :: thesis: t in rng (FD . s)

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_{1}[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: verum

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

hereby :: thesis: ( t in H_{1}(s) implies t in rng (FD . s) )

assume
t in Hassume
t in rng (FD . s)
; :: thesis: t in H_{1}(s)

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_{1}[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_{1}[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_{1}(s)
; :: thesis: verum

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

A15: dom (FD . s) = K . s by FUNCT_2:def 1;

reconsider u = u as set by TARSKI:1;

S

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

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

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

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: for r being object holds

( ( r in (f -extension_to_hom) .: Fs implies r in rng (Sups ) ) & ( r in rng (Sups ) implies r in (f -extension_to_hom) .: Fs ) )

then
(f -extension_to_hom) .: Fs = rng (Sups )
by TARSKI:2;( ( r in (f -extension_to_hom) .: Fs implies r in rng (Sups ) ) & ( r in rng (Sups ) implies r in (f -extension_to_hom) .: Fs ) )

let r be object ; :: thesis: ( ( r in (f -extension_to_hom) .: Fs implies r in rng (Sups ) ) & ( r in rng (Sups ) implies r in (f -extension_to_hom) .: Fs ) )

then consider s being Element of Fs9 such that

A25: r = Sup by WAYBEL_5:14;

S_{2}[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: verum

end;hereby :: thesis: ( r in rng (Sups ) implies r in (f -extension_to_hom) .: Fs )

assume
r in rng (Sups )
; :: thesis: r in (f -extension_to_hom) .: Fsassume
r in (f -extension_to_hom) .: Fs
; :: thesis: r in rng (Sups )

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_{2}[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: verum

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

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

then consider s being Element of Fs9 such that

A25: r = Sup by WAYBEL_5:14;

S

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

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

A27: now :: thesis: for r being object holds

( ( r in rng (Infs ) implies 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 } ) & ( 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 } implies r in rng (Infs ) ) )

for j being Element of Fs9 holds rng (FD . j) is directed
( ( r in rng (Infs ) implies 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 } ) & ( 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 } implies r in rng (Infs ) ) )

reconsider pdFD = product (doms FD) as non empty functional set ;

let r be object ; :: thesis: ( ( r in rng (Infs ) implies 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 } ) & ( 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 } implies r in rng (Infs ) ) )

reconsider dFFD = (product (doms FD)) --> Fs9 as ManySortedSet of pdFD ;

reconsider FFD = Frege FD as DoubleIndexedSet of dFFD,L ;

deffunc H_{2}( 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;

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in mFs } ; :: thesis: r in rng (Infs )

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 ;

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

( 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_{2}(s) )
by A29, YELLOW_2:def 6;

hence r in rng (Infs ) by A92, A84, WAYBEL_5:14; :: thesis: verum

end;let r be object ; :: thesis: ( ( r in rng (Infs ) implies 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 } ) & ( 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 } implies r in rng (Infs ) ) )

reconsider dFFD = (product (doms FD)) --> Fs9 as ManySortedSet of pdFD ;

reconsider FFD = Frege FD as DoubleIndexedSet of dFFD,L ;

deffunc H

( 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: for s being Element of pdFD holds rng (FFD . s) = H_{2}(s)

let s be Element of pdFD; :: thesis: rng (FFD . s) = H_{2}(s)

A30: dom FD = dom (FFD . s) by A28, WAYBEL_5:8;

_{2}(s)
by TARSKI:2; :: thesis: verum

end;A30: dom FD = dom (FFD . s) by A28, WAYBEL_5:8;

now :: thesis: for t being object holds

( ( t in rng (FFD . s) implies t in H_{2}(s) ) & ( t in H_{2}(s) implies t in rng (FFD . s) ) )

hence
rng (FFD . s) = H( ( t in rng (FFD . s) implies t in H

let t be object ; :: thesis: ( ( t in rng (FFD . s) implies t in H_{2}(s) ) & ( t in H_{2}(s) implies t in rng (FFD . s) ) )

_{2}(s)
; :: thesis: t in rng (FFD . s)

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_{1}[g . v,v,u]
by A7;

dom (FD . u) = K . u by FUNCT_2:def 1;

then S_{1}[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: verum

end;hereby :: thesis: ( t in H_{2}(s) implies t in rng (FFD . s) )

assume
t in Hassume
t in rng (FFD . s)
; :: thesis: t in H_{2}(s)

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_{1}[g . v,v,u]
by A7;

dom (FD . u) = K . u by FUNCT_2:def 1;

then S_{1}[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_{2}(s)
by A31, A32, A33, A34; :: thesis: verum

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

dom (FD . u) = K . u by FUNCT_2:def 1;

then S

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

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

dom (FD . u) = K . u by FUNCT_2:def 1;

then S

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

hereby :: thesis: ( 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 } implies r in rng (Infs ) )

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 } implies r in rng (Infs ) )

assume
r in rng (Infs )
; :: thesis: 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 }

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_{2}(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

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;

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

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_{2}(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: verum

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

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: ( not 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) } or t in bool the carrier of L )

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: t in bool the carrier of L

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

end;( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } or t in bool the carrier of L )

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: t in bool the carrier of L

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

hence
t in bool the carrier of L
; :: thesis: verum
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in tt or v in the carrier of L )

assume v in tt ; :: thesis: v in the carrier of L

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

end;assume v in tt ; :: thesis: v in the carrier of L

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

now :: thesis: for t being object holds

( ( t in H_{2}(s) implies 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) } } ) & ( 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) } } implies t in H_{2}(s) ) )

then A50:
H( ( t in H

( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } } ) & ( 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) } } implies t in H

let t be object ; :: thesis: ( ( t in H_{2}(s) implies 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) } } ) & ( 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) } } implies t in H_{2}(s) ) )

( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } } ; :: thesis: t in H_{2}(s)

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_{2}(s)
by A48; :: thesis: verum

end;( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } } ) & ( 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) } } implies t in H

hereby :: thesis: ( 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) } } implies t in H_{2}(s) )

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) } } implies t in H

assume
t in H_{2}(s)
; :: thesis: 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) } }

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

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

end;( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } }

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

then reconsider Y1 = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } or v in the carrier of L )

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: v in the carrier of L

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

end;( x = {z} & z in s . u ) } or v in the carrier of L )

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: v in the carrier of L

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

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

( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } } ; :: thesis: t in H

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

( 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

then reconsider Y = union (rng s) as Subset of X ;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in union (rng s) or t in X )

assume t in union (rng s) ; :: thesis: t in X

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

end;assume t in union (rng s) ; :: thesis: t in X

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

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: for t being object holds

( ( 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) } implies t in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

( x = {z} & z in Y ) } implies 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) } ) )

then A75:
union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( ( 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) } implies t in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

( x = {z} & z in Y ) } implies 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) } ) )

let t be object ; :: thesis: ( ( 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) } implies t in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

( x = {z} & z in Y ) } implies 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) } ) )

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

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

end;( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } implies t in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

( x = {z} & z in Y ) } implies 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) } ) )

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

( x = {z} & z in Y ) } implies 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) } )

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

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

end;( x = {z} & z in s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } ; :: thesis: t 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 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: verum

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

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

( 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: for Z being set st Z in Fs9 holds

Y in Z

then
Y in mFs
by SETFAM_1:def 1;Y in Z

reconsider Y9 = Y as Element of (BoolePoset X) by A3, YELLOW_1:4;

let Z be set ; :: thesis: ( Z in Fs9 implies Y in Z )

assume A76: Z in Fs9 ; :: thesis: Y in Z

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

end;let Z be set ; :: thesis: ( Z in Fs9 implies Y in Z )

assume A76: Z in Fs9 ; :: thesis: Y in Z

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

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

.= "/\" ((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: verum

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in mFs } ; :: thesis: r in rng (Infs )

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: for w being object st w in dom (doms FD) holds

(Fs9 --> Y) . w in (doms FD) . w

set s9 = Fs9 --> Y;(Fs9 --> Y) . w in (doms FD) . w

let w be object ; :: thesis: ( w in dom (doms FD) implies (Fs9 --> Y) . w in (doms FD) . w )

assume A87: w in dom (doms FD) ; :: thesis: (Fs9 --> Y) . w in (doms FD) . w

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

end;assume A87: w in dom (doms FD) ; :: thesis: (Fs9 --> Y) . w in (doms FD) . w

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

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

now :: thesis: for t being object holds

( ( t in H_{2}(s) implies t in {r} ) & ( t in {r} implies t in H_{2}(s) ) )

then A92:
{ ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( ( t in H

set u = the Element of Fs9;

let t be object ; :: thesis: ( ( t in H_{2}(s) implies t in {r} ) & ( t in {r} implies t in H_{2}(s) ) )

A89: ( dom (Fs9 --> Y) = Fs9 & s . the Element of Fs9 = Y ) ;

_{2}(s)

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_{2}(s)
by A82, A91, A89; :: thesis: verum

end;let t be object ; :: thesis: ( ( t in H

A89: ( dom (Fs9 --> Y) = Fs9 & s . the Element of Fs9 = Y ) ;

hereby :: thesis: ( t in {r} implies t in H_{2}(s) )

assume
t in {r}
; :: thesis: t in Hassume
t in H_{2}(s)
; :: thesis: t in {r}

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

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

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

( 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

hence r in rng (Infs ) by A92, A84, WAYBEL_5:14; :: thesis: verum

proof

then A115: Inf =
Sup
by WAYBEL_5:19
let j be Element of Fs9; :: thesis: rng (FD . j) is directed

let k, m be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not k in rng (FD . j) or not m in rng (FD . j) or ex b_{1} being Element of the carrier of L st

( b_{1} in rng (FD . j) & k <= b_{1} & m <= b_{1} ) )

assume that

A93: k in rng (FD . j) and

A94: m in rng (FD . j) ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in rng (FD . j) & k <= b_{1} & m <= b_{1} )

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_{1}[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_{1}[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: ( n in rng (FD . j) & k <= n & m <= n )

thus n in rng (FD . j) by A100, A99, A101, FUNCT_1:def 3; :: thesis: ( k <= n & m <= n )

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

( 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 ) }_{1}[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: m <= n

S_{1}[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: verum

end;let k, m be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not k in rng (FD . j) or not m in rng (FD . j) or ex b

( b

assume that

A93: k in rng (FD . j) and

A94: m in rng (FD . j) ; :: thesis: ex b

( b

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

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

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: ( n in rng (FD . j) & k <= n & m <= n )

thus n in rng (FD . j) by A100, A99, A101, FUNCT_1:def 3; :: thesis: ( k <= n & m <= n )

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

A111:
ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

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

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: w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

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

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

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

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: w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

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

( 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

S
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

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

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: w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

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 kd ) } by A113; :: thesis: verum

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

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

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: w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

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

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 kd ) } by A113; :: thesis: verum

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: m <= n

S

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

.= "\/" ((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: verum