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))); WAYBEL_0:def 32 f -extension_to_hom preserves_inf_of Fs
assume
ex_inf_of Fs, InclPoset (Filt (BoolePoset X))
; WAYBEL_0:def 30 ( 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; "/\" (((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 )
;
suppose
not
Fs is
empty
;
"/\" (((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 S1[
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 H1(
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
non-empty 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 &
S1[
y,
s,
i] )
proof
let i be
object ;
( 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 & S1[y,s,i] ) )
assume A6:
i in Fs9
;
for s being object st s in K . i holds
ex y being object st
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] )
let s be
object ;
( s in K . i implies ex y being object st
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] ) )
assume
s in K . i
;
ex y being object st
( y in (Fs9 --> the carrier of L) . i & S1[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);
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] )
y in the
carrier of
L
;
hence
y in (Fs9 --> the carrier of L) . i
by A6, FUNCOP_1:7;
S1[y,s,i]
take
D2
;
( 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
;
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)
;
verum
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
S1[
g . s,
s,
i] ) )
from MSSUBFAM:sch 1(A5);
defpred S2[
Element of
Fs9]
means rng (FD . X) = H1(
X);
A8:
for
s being
Element of
Fs9 holds
S2[
s]
proof
let s be
Element of
Fs9;
S2[s]
now for t being object holds
( ( t in rng (FD . s) implies t in H1(s) ) & ( t in H1(s) implies t in rng (FD . s) ) )let t be
object ;
( ( t in rng (FD . s) implies t in H1(s) ) & ( t in H1(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
S1[
g . u,
u,
s]
by A7;
hereby ( t in H1(s) implies t in rng (FD . s) )
assume
t in rng (FD . s)
;
t in H1(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
S1[
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;
S1[
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 H1(
s)
;
verum
end; assume
t in H1(
s)
;
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;
S1[
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;
verum end;
hence
S2[
s]
by TARSKI:2;
verum
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 ;
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 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 ) ) )reconsider pdFD =
product (doms FD) as non
empty functional set ;
let r be
object ;
( ( 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 H2(
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 for s being Element of pdFD holds rng (FFD . s) = H2(s)let s be
Element of
pdFD;
rng (FFD . s) = H2(s)A30:
dom FD = dom (FFD . s)
by A28, WAYBEL_5:8;
now for t being object holds
( ( t in rng (FFD . s) implies t in H2(s) ) & ( t in H2(s) implies t in rng (FFD . s) ) )let t be
object ;
( ( t in rng (FFD . s) implies t in H2(s) ) & ( t in H2(s) implies t in rng (FFD . s) ) )hereby ( t in H2(s) implies t in rng (FFD . s) )
assume
t in rng (FFD . s)
;
t in H2(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
S1[
g . v,
v,
u]
by A7;
dom (FD . u) = K . u
by FUNCT_2:def 1;
then
S1[
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 H2(
s)
by A31, A32, A33, A34;
verum
end; assume
t in H2(
s)
;
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
S1[
g . v,
v,
u]
by A7;
dom (FD . u) = K . u
by FUNCT_2:def 1;
then
S1[
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;
verum end; hence
rng (FFD . s) = H2(
s)
by TARSKI:2;
verum end; hereby ( 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 )
;
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
then A50:
H2(
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 ;
TARSKI:def 3 ( not t in union (rng s) or t in X )
assume
t in union (rng s)
;
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;
verum
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;
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 for Z being set st Z in Fs9 holds
Y in Zreconsider Y9 =
Y as
Element of
(BoolePoset X) by A3, YELLOW_1:4;
let Z be
set ;
( Z in Fs9 implies Y in Z )assume A76:
Z in Fs9
;
Y in Zthen
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;
verum 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) =
"/\" (
H2(
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;
verum
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 }
;
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 for w being object st w in dom (doms FD) holds
(Fs9 --> Y) . w in (doms FD) . wlet w be
object ;
( w in dom (doms FD) implies (Fs9 --> Y) . w in (doms FD) . w )assume A87:
w in dom (doms FD)
;
(Fs9 --> Y) . w in (doms FD) . wthen
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;
verum end; set s9 =
Fs9 --> Y;
reconsider s =
Fs9 --> Y as
Element of
pdFD by A85, A86, CARD_3:9;
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) = H2(
s) )
by A29, YELLOW_2:def 6;
hence
r in rng (Infs )
by A92, A84, WAYBEL_5:14;
verum end;
for
j being
Element of
Fs9 holds
rng (FD . j) is
directed
proof
let j be
Element of
Fs9;
rng (FD . j) is directed let k,
m be
Element of
L;
WAYBEL_0:def 1 ( not k in rng (FD . j) or not m in rng (FD . j) or ex b1 being Element of the carrier of L st
( b1 in rng (FD . j) & k <= b1 & m <= b1 ) )
assume that A93:
k in rng (FD . j)
and A94:
m in rng (FD . j)
;
ex b1 being Element of the carrier of L st
( b1 in rng (FD . j) & k <= b1 & m <= b1 )
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
S1[
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 ) } ;
S1[
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
;
( n in rng (FD . j) & k <= n & m <= n )
thus
n in rng (FD . j)
by A100, A99, A101, FUNCT_1:def 3;
( 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 ) }
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 ) }
S1[
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;
m <= n
S1[
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;
verum
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;
verum end;