let L be complete lim-inf TopLattice; :: thesis: for A being non empty Subset of L holds

( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds

lim_inf F in A )

let A be non empty Subset of L; :: thesis: ( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds

lim_inf F in A )

xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L)) by WAYBEL28:def 4;

then A1: xi L = { V where V is Subset of L : for p being Element of L st p in V holds

for N being net of L st [N,p] in lim_inf-Convergence L holds

N is_eventually_in V } by YELLOW_6:def 24;

set V = A ` ;

A2: the topology of L = xi L by Def2;

lim_inf F in A ; :: thesis: A is closed

then A ` is open by A2;

hence A is closed ; :: thesis: verum

( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds

lim_inf F in A )

let A be non empty Subset of L; :: thesis: ( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds

lim_inf F in A )

xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L)) by WAYBEL28:def 4;

then A1: xi L = { V where V is Subset of L : for p being Element of L st p in V holds

for N being net of L st [N,p] in lim_inf-Convergence L holds

N is_eventually_in V } by YELLOW_6:def 24;

set V = A ` ;

A2: the topology of L = xi L by Def2;

hereby :: thesis: ( ( for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds

lim_inf F in A ) implies A is closed )

assume A14:
for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds lim_inf F in A ) implies A is closed )

assume
A is closed
; :: thesis: for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds

lim_inf F in A

then A ` in xi L by A2, PRE_TOPC:def 2;

then A3: ex V being Subset of L st

( V = A ` & ( for p being Element of L st p in V holds

for N being net of L st [N,p] in lim_inf-Convergence L holds

N is_eventually_in V ) ) by A1;

let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: ( A in F implies lim_inf F in A )

assume A4: A in F ; :: thesis: lim_inf F in A

( ( for M being subnet of a_net F holds lim_inf F = lim_inf M ) & a_net F in NetUniv L ) by Th14, Th16;

then A5: [(a_net F),(lim_inf F)] in lim_inf-Convergence L by WAYBEL28:def 3;

assume not lim_inf F in A ; :: thesis: contradiction

then lim_inf F in A ` by XBOOLE_0:def 5;

then a_net F is_eventually_in A ` by A3, A5;

then consider i being Element of (a_net F) such that

A6: for j being Element of (a_net F) st i <= j holds

(a_net F) . j in A ` ;

A7: the carrier of (a_net F) = { [a,f] where a is Element of L, f is Element of F : a in f } by YELLOW19:def 4;

i in the carrier of (a_net F) ;

then consider a being Element of L, f being Element of F such that

A8: i = [a,f] and

a in f by A7;

reconsider A9 = A, f9 = f as Element of (BoolePoset ([#] L)) by A4;

consider B being Element of (BoolePoset ([#] L)) such that

A9: B in F and

A10: A9 >= B and

A11: f9 >= B by A4, WAYBEL_0:def 2;

set b = the Element of B;

not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;

then not B is empty by A9, YELLOW_1:18;

then A12: the Element of B in B ;

the carrier of (BoolePoset ([#] L)) = bool the carrier of L by WAYBEL_7:2;

then [ the Element of B,B] in the carrier of (a_net F) by A7, A9, A12;

then reconsider j = [ the Element of B,B] as Element of (a_net F) ;

B c= f by A11, YELLOW_1:2;

then j `2 c= f ;

then j `2 c= i `2 by A8;

then j >= i by YELLOW19:def 4;

then (a_net F) . j in A ` by A6;

then j `1 in A ` by YELLOW19:def 4;

then A13: the Element of B in A ` ;

B c= A by A10, YELLOW_1:2;

hence contradiction by A12, A13, XBOOLE_0:def 5; :: thesis: verum

end;lim_inf F in A

then A ` in xi L by A2, PRE_TOPC:def 2;

then A3: ex V being Subset of L st

( V = A ` & ( for p being Element of L st p in V holds

for N being net of L st [N,p] in lim_inf-Convergence L holds

N is_eventually_in V ) ) by A1;

let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: ( A in F implies lim_inf F in A )

assume A4: A in F ; :: thesis: lim_inf F in A

( ( for M being subnet of a_net F holds lim_inf F = lim_inf M ) & a_net F in NetUniv L ) by Th14, Th16;

then A5: [(a_net F),(lim_inf F)] in lim_inf-Convergence L by WAYBEL28:def 3;

assume not lim_inf F in A ; :: thesis: contradiction

then lim_inf F in A ` by XBOOLE_0:def 5;

then a_net F is_eventually_in A ` by A3, A5;

then consider i being Element of (a_net F) such that

A6: for j being Element of (a_net F) st i <= j holds

(a_net F) . j in A ` ;

A7: the carrier of (a_net F) = { [a,f] where a is Element of L, f is Element of F : a in f } by YELLOW19:def 4;

i in the carrier of (a_net F) ;

then consider a being Element of L, f being Element of F such that

A8: i = [a,f] and

a in f by A7;

reconsider A9 = A, f9 = f as Element of (BoolePoset ([#] L)) by A4;

consider B being Element of (BoolePoset ([#] L)) such that

A9: B in F and

A10: A9 >= B and

A11: f9 >= B by A4, WAYBEL_0:def 2;

set b = the Element of B;

not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;

then not B is empty by A9, YELLOW_1:18;

then A12: the Element of B in B ;

the carrier of (BoolePoset ([#] L)) = bool the carrier of L by WAYBEL_7:2;

then [ the Element of B,B] in the carrier of (a_net F) by A7, A9, A12;

then reconsider j = [ the Element of B,B] as Element of (a_net F) ;

B c= f by A11, YELLOW_1:2;

then j `2 c= f ;

then j `2 c= i `2 by A8;

then j >= i by YELLOW19:def 4;

then (a_net F) . j in A ` by A6;

then j `1 in A ` by YELLOW19:def 4;

then A13: the Element of B in A ` ;

B c= A by A10, YELLOW_1:2;

hence contradiction by A12, A13, XBOOLE_0:def 5; :: thesis: verum

lim_inf F in A ; :: thesis: A is closed

now :: thesis: for p being Element of L st p in A ` holds

for N being net of L st [N,p] in lim_inf-Convergence L holds

N is_eventually_in A `

then
A ` in xi L
by A1;for N being net of L st [N,p] in lim_inf-Convergence L holds

N is_eventually_in A `

let p be Element of L; :: thesis: ( p in A ` implies for N being net of L st [N,p] in lim_inf-Convergence L holds

N is_eventually_in A ` )

assume p in A ` ; :: thesis: for N being net of L st [N,p] in lim_inf-Convergence L holds

N is_eventually_in A `

then A15: not p in (A `) ` by XBOOLE_0:def 5;

reconsider x = p as Element of L ;

let N be net of L; :: thesis: ( [N,p] in lim_inf-Convergence L implies N is_eventually_in A ` )

assume A16: [N,p] in lim_inf-Convergence L ; :: thesis: N is_eventually_in A `

assume not N is_eventually_in A ` ; :: thesis: contradiction

then N is_often_in A by WAYBEL_0:10;

then consider N9 being strict subnet of N such that

A17: rng the mapping of N9 c= A and

A18: N9 is SubNetStr of N by Th17;

lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def 18;

then A19: N in NetUniv L by A16, ZFMISC_1:87;

then A20: ex N1 being strict net of L st

( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by YELLOW_6:def 11;

set j0 = the Element of N9;

reconsider rj = rng the mapping of (N9 | the Element of N9), a = A as Element of (BoolePoset ([#] L)) by WAYBEL_7:2;

set j2 = the Element of N9;

set G = { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ;

set g = rng the mapping of (N9 | the Element of N9);

A21: rng the mapping of (N9 | the Element of N9) in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ;

for g being object st g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } holds

g in the carrier of (BoolePoset ([#] L))

A22: G c= fininfs G by WAYBEL_0:50;

then rj c= a by A17;

then ( rng the mapping of (N9 | the Element of N9) in G & rj <= a ) by YELLOW_1:2;

then A26: a in uparrow (fininfs G) by A22, WAYBEL_0:def 16;

A27: x = lim_inf N9 by A16, A19, WAYBEL28:def 3;

then A28: x = "\/" ( { (inf (N9 | j)) where j is Element of N9 : verum } ,L) by Th11;

the carrier of N9 c= the carrier of N by A18, YELLOW_6:10;

then the carrier of N9 in the_universe_of the carrier of L by A20, CLASSES1:def 1;

then A29: N9 in NetUniv L by YELLOW_6:def 11;

A30: not {} in fininfs G

not y in fininfs G

then uparrow (fininfs G) is proper ;

then consider F being Filter of (BoolePoset ([#] L)) such that

A50: uparrow (fininfs G) c= F and

A51: F is ultra by WAYBEL_7:26;

A52: fininfs G c= uparrow (fininfs G) by WAYBEL_0:16;

A53: { (inf (N9 | j)) where j is Element of N9 : verum } c= { (inf f) where f is Subset of L : f in F }

x = lim_inf M ;

{ (inf f) where f is Subset of L : f in F } is_<=_than x

( ex_sup_of { (inf f) where f is Subset of L : f in F } ,L & ex_sup_of { (inf (N9 | j)) where j is Element of N9 : verum } ,L ) by YELLOW_0:17;

then x <= lim_inf F by A28, A53, YELLOW_0:34;

then x = lim_inf F by A73, YELLOW_0:def 3;

hence contradiction by A14, A50, A51, A26, A15; :: thesis: verum

end;N is_eventually_in A ` )

assume p in A ` ; :: thesis: for N being net of L st [N,p] in lim_inf-Convergence L holds

N is_eventually_in A `

then A15: not p in (A `) ` by XBOOLE_0:def 5;

reconsider x = p as Element of L ;

let N be net of L; :: thesis: ( [N,p] in lim_inf-Convergence L implies N is_eventually_in A ` )

assume A16: [N,p] in lim_inf-Convergence L ; :: thesis: N is_eventually_in A `

assume not N is_eventually_in A ` ; :: thesis: contradiction

then N is_often_in A by WAYBEL_0:10;

then consider N9 being strict subnet of N such that

A17: rng the mapping of N9 c= A and

A18: N9 is SubNetStr of N by Th17;

lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def 18;

then A19: N in NetUniv L by A16, ZFMISC_1:87;

then A20: ex N1 being strict net of L st

( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by YELLOW_6:def 11;

set j0 = the Element of N9;

reconsider rj = rng the mapping of (N9 | the Element of N9), a = A as Element of (BoolePoset ([#] L)) by WAYBEL_7:2;

set j2 = the Element of N9;

set G = { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ;

set g = rng the mapping of (N9 | the Element of N9);

A21: rng the mapping of (N9 | the Element of N9) in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ;

for g being object st g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } holds

g in the carrier of (BoolePoset ([#] L))

proof

then reconsider G = { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } as non empty Subset of (BoolePoset ([#] L)) by A21, TARSKI:def 3;
let g be object ; :: thesis: ( g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } implies g in the carrier of (BoolePoset ([#] L)) )

assume g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ; :: thesis: g in the carrier of (BoolePoset ([#] L))

then ex j3 being Element of N9 st g = rng the mapping of (N9 | j3) ;

then g in bool ([#] L) ;

hence g in the carrier of (BoolePoset ([#] L)) by WAYBEL_7:2; :: thesis: verum

end;assume g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ; :: thesis: g in the carrier of (BoolePoset ([#] L))

then ex j3 being Element of N9 st g = rng the mapping of (N9 | j3) ;

then g in bool ([#] L) ;

hence g in the carrier of (BoolePoset ([#] L)) by WAYBEL_7:2; :: thesis: verum

A22: G c= fininfs G by WAYBEL_0:50;

now :: thesis: for p being object st p in rj holds

p in rng the mapping of N9

then
rj c= rng the mapping of N9
;p in rng the mapping of N9

let p be object ; :: thesis: ( p in rj implies p in rng the mapping of N9 )

assume p in rj ; :: thesis: p in rng the mapping of N9

then p in rng ( the mapping of N9 | the carrier of (N9 | the Element of N9)) by WAYBEL_9:def 7;

then consider q being object such that

A23: q in dom ( the mapping of N9 | the carrier of (N9 | the Element of N9)) and

A24: p = ( the mapping of N9 | the carrier of (N9 | the Element of N9)) . q by FUNCT_1:def 3;

q in (dom the mapping of N9) /\ the carrier of (N9 | the Element of N9) by A23, RELAT_1:61;

then A25: q in dom the mapping of N9 by XBOOLE_0:def 4;

p = the mapping of N9 . q by A23, A24, FUNCT_1:47;

hence p in rng the mapping of N9 by A25, FUNCT_1:3; :: thesis: verum

end;assume p in rj ; :: thesis: p in rng the mapping of N9

then p in rng ( the mapping of N9 | the carrier of (N9 | the Element of N9)) by WAYBEL_9:def 7;

then consider q being object such that

A23: q in dom ( the mapping of N9 | the carrier of (N9 | the Element of N9)) and

A24: p = ( the mapping of N9 | the carrier of (N9 | the Element of N9)) . q by FUNCT_1:def 3;

q in (dom the mapping of N9) /\ the carrier of (N9 | the Element of N9) by A23, RELAT_1:61;

then A25: q in dom the mapping of N9 by XBOOLE_0:def 4;

p = the mapping of N9 . q by A23, A24, FUNCT_1:47;

hence p in rng the mapping of N9 by A25, FUNCT_1:3; :: thesis: verum

then rj c= a by A17;

then ( rng the mapping of (N9 | the Element of N9) in G & rj <= a ) by YELLOW_1:2;

then A26: a in uparrow (fininfs G) by A22, WAYBEL_0:def 16;

A27: x = lim_inf N9 by A16, A19, WAYBEL28:def 3;

then A28: x = "\/" ( { (inf (N9 | j)) where j is Element of N9 : verum } ,L) by Th11;

the carrier of N9 c= the carrier of N by A18, YELLOW_6:10;

then the carrier of N9 in the_universe_of the carrier of L by A20, CLASSES1:def 1;

then A29: N9 in NetUniv L by YELLOW_6:def 11;

A30: not {} in fininfs G

proof

for y being Element of (BoolePoset ([#] L)) st Bottom (BoolePoset ([#] L)) >= y holds
assume
{} in fininfs G
; :: thesis: contradiction

then consider Y being finite Subset of G such that

A31: {} = "/\" (Y,(BoolePoset ([#] L))) and

ex_inf_of Y, BoolePoset ([#] L) ;

defpred S_{1}[ object , object ] means ex j being Element of N9 st

( j = $2 & $1 = rng the mapping of (N9 | j) );

A32: "/\" ({},(BoolePoset ([#] L))) = Top (BoolePoset ([#] L)) by YELLOW_0:def 12

.= [#] L by YELLOW_1:19 ;

reconsider Y = Y as finite Subset of (BoolePoset ([#] L)) by XBOOLE_1:1;

A33: for x being object st x in Y holds

ex y being object st

( y in the carrier of N9 & S_{1}[x,y] )

A35: ( dom f = Y & rng f c= the carrier of N9 ) and

A36: for x being object st x in Y holds

S_{1}[x,f . x]
from FUNCT_1:sch 6(A33);

reconsider C = rng f as finite Subset of ([#] N9) by A35, FINSET_1:8;

[#] N9 is directed by WAYBEL_0:def 6;

then consider j0 being Element of N9 such that

j0 in [#] N9 and

A37: j0 is_>=_than C by WAYBEL_0:1;

for y being set st y in Y holds

rng the mapping of (N9 | j0) c= y

then rng the mapping of (N9 | j0) c= {} by A31, A32, YELLOW_1:20;

hence contradiction ; :: thesis: verum

end;then consider Y being finite Subset of G such that

A31: {} = "/\" (Y,(BoolePoset ([#] L))) and

ex_inf_of Y, BoolePoset ([#] L) ;

defpred S

( j = $2 & $1 = rng the mapping of (N9 | j) );

A32: "/\" ({},(BoolePoset ([#] L))) = Top (BoolePoset ([#] L)) by YELLOW_0:def 12

.= [#] L by YELLOW_1:19 ;

reconsider Y = Y as finite Subset of (BoolePoset ([#] L)) by XBOOLE_1:1;

A33: for x being object st x in Y holds

ex y being object st

( y in the carrier of N9 & S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in Y implies ex y being object st

( y in the carrier of N9 & S_{1}[x,y] ) )

assume x in Y ; :: thesis: ex y being object st

( y in the carrier of N9 & S_{1}[x,y] )

then x in G ;

then A34: ex j being Element of N9 st x = rng the mapping of (N9 | j) ;

assume for y being object st y in the carrier of N9 holds

not S_{1}[x,y]
; :: thesis: contradiction

hence contradiction by A34; :: thesis: verum

end;( y in the carrier of N9 & S

assume x in Y ; :: thesis: ex y being object st

( y in the carrier of N9 & S

then x in G ;

then A34: ex j being Element of N9 st x = rng the mapping of (N9 | j) ;

assume for y being object st y in the carrier of N9 holds

not S

hence contradiction by A34; :: thesis: verum

A35: ( dom f = Y & rng f c= the carrier of N9 ) and

A36: for x being object st x in Y holds

S

reconsider C = rng f as finite Subset of ([#] N9) by A35, FINSET_1:8;

[#] N9 is directed by WAYBEL_0:def 6;

then consider j0 being Element of N9 such that

j0 in [#] N9 and

A37: j0 is_>=_than C by WAYBEL_0:1;

for y being set st y in Y holds

rng the mapping of (N9 | j0) c= y

proof

then
rng the mapping of (N9 | j0) c= meet Y
by A31, A32, SETFAM_1:5;
let y be set ; :: thesis: ( y in Y implies rng the mapping of (N9 | j0) c= y )

assume A38: y in Y ; :: thesis: rng the mapping of (N9 | j0) c= y

consider j1 being Element of N9 such that

A39: j1 = f . y and

A40: y = rng the mapping of (N9 | j1) by A36, A38;

A41: f . y in rng f by A35, A38, FUNCT_1:3;

then reconsider f1 = f . y as Element of N9 by A35;

A42: f1 <= j0 by A37, A41;

for p being object st p in rng the mapping of (N9 | j0) holds

p in y

end;assume A38: y in Y ; :: thesis: rng the mapping of (N9 | j0) c= y

consider j1 being Element of N9 such that

A39: j1 = f . y and

A40: y = rng the mapping of (N9 | j1) by A36, A38;

A41: f . y in rng f by A35, A38, FUNCT_1:3;

then reconsider f1 = f . y as Element of N9 by A35;

A42: f1 <= j0 by A37, A41;

for p being object st p in rng the mapping of (N9 | j0) holds

p in y

proof

hence
rng the mapping of (N9 | j0) c= y
; :: thesis: verum
let p be object ; :: thesis: ( p in rng the mapping of (N9 | j0) implies p in y )

assume p in rng the mapping of (N9 | j0) ; :: thesis: p in y

then p in rng ( the mapping of N9 | the carrier of (N9 | j0)) by WAYBEL_9:def 7;

then consider q being object such that

A43: q in dom ( the mapping of N9 | the carrier of (N9 | j0)) and

A44: p = ( the mapping of N9 | the carrier of (N9 | j0)) . q by FUNCT_1:def 3;

A45: q in (dom the mapping of N9) /\ the carrier of (N9 | j0) by A43, RELAT_1:61;

then q in the carrier of (N9 | j0) by XBOOLE_0:def 4;

then q in { n9 where n9 is Element of N9 : j0 <= n9 } by WAYBEL_9:12;

then consider n9 being Element of N9 such that

A46: q = n9 and

A47: j0 <= n9 ;

f1 <= n9 by A42, A47, YELLOW_0:def 2;

then q in { m9 where m9 is Element of N9 : j1 <= m9 } by A39, A46;

then A48: q in the carrier of (N9 | j1) by WAYBEL_9:12;

q in dom the mapping of N9 by A45, XBOOLE_0:def 4;

then q in (dom the mapping of N9) /\ the carrier of (N9 | j1) by A48, XBOOLE_0:def 4;

then A49: q in dom ( the mapping of N9 | the carrier of (N9 | j1)) by RELAT_1:61;

p = the mapping of N9 . q by A43, A44, FUNCT_1:47;

then p = ( the mapping of N9 | the carrier of (N9 | j1)) . q by A49, FUNCT_1:47;

then p in rng ( the mapping of N9 | the carrier of (N9 | j1)) by A49, FUNCT_1:3;

hence p in y by A40, WAYBEL_9:def 7; :: thesis: verum

end;assume p in rng the mapping of (N9 | j0) ; :: thesis: p in y

then p in rng ( the mapping of N9 | the carrier of (N9 | j0)) by WAYBEL_9:def 7;

then consider q being object such that

A43: q in dom ( the mapping of N9 | the carrier of (N9 | j0)) and

A44: p = ( the mapping of N9 | the carrier of (N9 | j0)) . q by FUNCT_1:def 3;

A45: q in (dom the mapping of N9) /\ the carrier of (N9 | j0) by A43, RELAT_1:61;

then q in the carrier of (N9 | j0) by XBOOLE_0:def 4;

then q in { n9 where n9 is Element of N9 : j0 <= n9 } by WAYBEL_9:12;

then consider n9 being Element of N9 such that

A46: q = n9 and

A47: j0 <= n9 ;

f1 <= n9 by A42, A47, YELLOW_0:def 2;

then q in { m9 where m9 is Element of N9 : j1 <= m9 } by A39, A46;

then A48: q in the carrier of (N9 | j1) by WAYBEL_9:12;

q in dom the mapping of N9 by A45, XBOOLE_0:def 4;

then q in (dom the mapping of N9) /\ the carrier of (N9 | j1) by A48, XBOOLE_0:def 4;

then A49: q in dom ( the mapping of N9 | the carrier of (N9 | j1)) by RELAT_1:61;

p = the mapping of N9 . q by A43, A44, FUNCT_1:47;

then p = ( the mapping of N9 | the carrier of (N9 | j1)) . q by A49, FUNCT_1:47;

then p in rng ( the mapping of N9 | the carrier of (N9 | j1)) by A49, FUNCT_1:3;

hence p in y by A40, WAYBEL_9:def 7; :: thesis: verum

then rng the mapping of (N9 | j0) c= {} by A31, A32, YELLOW_1:20;

hence contradiction ; :: thesis: verum

not y in fininfs G

proof

then
not Bottom (BoolePoset ([#] L)) in uparrow (fininfs G)
by WAYBEL_0:def 16;
let y be Element of (BoolePoset ([#] L)); :: thesis: ( Bottom (BoolePoset ([#] L)) >= y implies not y in fininfs G )

assume Bottom (BoolePoset ([#] L)) >= y ; :: thesis: not y in fininfs G

then ( {} = Bottom (BoolePoset ([#] L)) & y c= Bottom (BoolePoset ([#] L)) ) by YELLOW_1:2, YELLOW_1:18;

hence not y in fininfs G by A30; :: thesis: verum

end;assume Bottom (BoolePoset ([#] L)) >= y ; :: thesis: not y in fininfs G

then ( {} = Bottom (BoolePoset ([#] L)) & y c= Bottom (BoolePoset ([#] L)) ) by YELLOW_1:2, YELLOW_1:18;

hence not y in fininfs G by A30; :: thesis: verum

then uparrow (fininfs G) is proper ;

then consider F being Filter of (BoolePoset ([#] L)) such that

A50: uparrow (fininfs G) c= F and

A51: F is ultra by WAYBEL_7:26;

A52: fininfs G c= uparrow (fininfs G) by WAYBEL_0:16;

A53: { (inf (N9 | j)) where j is Element of N9 : verum } c= { (inf f) where f is Subset of L : f in F }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (inf (N9 | j)) where j is Element of N9 : verum } or x in { (inf f) where f is Subset of L : f in F } )

assume x in { (inf (N9 | j)) where j is Element of N9 : verum } ; :: thesis: x in { (inf f) where f is Subset of L : f in F }

then consider j3 being Element of N9 such that

A54: x = inf (N9 | j3) ;

reconsider f1 = rng the mapping of (N9 | j3) as Subset of L ;

fininfs G c= F by A50, A52;

then A55: ( f1 in G & G c= F ) by A22;

x = Inf by A54, WAYBEL_9:def 2

.= "/\" ((rng the mapping of (N9 | j3)),L) by YELLOW_2:def 6 ;

hence x in { (inf f) where f is Subset of L : f in F } by A55; :: thesis: verum

end;assume x in { (inf (N9 | j)) where j is Element of N9 : verum } ; :: thesis: x in { (inf f) where f is Subset of L : f in F }

then consider j3 being Element of N9 such that

A54: x = inf (N9 | j3) ;

reconsider f1 = rng the mapping of (N9 | j3) as Subset of L ;

fininfs G c= F by A50, A52;

then A55: ( f1 in G & G c= F ) by A22;

x = Inf by A54, WAYBEL_9:def 2

.= "/\" ((rng the mapping of (N9 | j3)),L) by YELLOW_2:def 6 ;

hence x in { (inf f) where f is Subset of L : f in F } by A55; :: thesis: verum

now :: thesis: for M being subnet of N9 holds x = lim_inf M

then A56:
for M being subnet of N9 st M in NetUniv L holds let M be subnet of N9; :: thesis: x = lim_inf M

M is subnet of N by YELLOW_6:15;

hence x = lim_inf M by A16, A19, WAYBEL28:def 3; :: thesis: verum

end;M is subnet of N by YELLOW_6:15;

hence x = lim_inf M by A16, A19, WAYBEL28:def 3; :: thesis: verum

x = lim_inf M ;

{ (inf f) where f is Subset of L : f in F } is_<=_than x

proof

then A73:
lim_inf F <= x
by YELLOW_0:32;
let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in { (inf f) where f is Subset of L : f in F } or y <= x )

assume y in { (inf f) where f is Subset of L : f in F } ; :: thesis: y <= x

then consider f0 being Subset of L such that

A57: y = inf f0 and

A58: f0 in F ;

defpred S_{1}[ Element of N9, Element of N9] means ( $1 <= $2 & N9 . $2 in f0 );

A67: for j being Element of N9 holds S_{1}[j,p . j]
from FUNCT_2:sch 3(A59);

for b being object st b in rng the mapping of (N9 * p) holds

b in f0

then A70: "/\" (f0,L) <= "/\" ((rng the mapping of (N9 * p)),L) by WAYBEL_7:1;

A71: for M being subnet of N9 st M in NetUniv L holds

x >= inf M by A29, A56, WAYBEL28:3;

p is greater_or_equal_to_id by A67, WAYBEL28:def 1;

then A72: inf (N9 * p) <= x by A29, A27, A71, WAYBEL28:13;

inf (N9 * p) = Inf by WAYBEL_9:def 2

.= "/\" ((rng the mapping of (N9 * p)),L) by YELLOW_2:def 6 ;

hence y <= x by A57, A72, A70, YELLOW_0:def 2; :: thesis: verum

end;assume y in { (inf f) where f is Subset of L : f in F } ; :: thesis: y <= x

then consider f0 being Subset of L such that

A57: y = inf f0 and

A58: f0 in F ;

defpred S

A59: now :: thesis: for j being Element of N9 ex pj being Element of N9 st S_{1}[j,pj]

consider p being Function of N9,N9 such that let j be Element of N9; :: thesis: ex pj being Element of N9 st S_{1}[j,pj]

not Bottom (BoolePoset ([#] L)) in F by A51, WAYBEL_7:4;

then A60: not {} in F by YELLOW_1:18;

G c= uparrow (fininfs G) by A22, A52;

then A61: G c= F by A50;

rng the mapping of (N9 | j) in G ;

then f0 /\ (rng the mapping of (N9 | j)) in F by A58, A61, WAYBEL_7:9;

then consider nj being Element of L such that

A62: nj in f0 /\ (rng the mapping of (N9 | j)) by A60, SUBSET_1:4;

nj in rng the mapping of (N9 | j) by A62, XBOOLE_0:def 4;

then consider pj9 being object such that

A63: pj9 in dom the mapping of (N9 | j) and

A64: nj = the mapping of (N9 | j) . pj9 by FUNCT_1:def 3;

pj9 in the carrier of (N9 | j) by A63;

then pj9 in { y9 where y9 is Element of N9 : j <= y9 } by WAYBEL_9:12;

then consider pj being Element of N9 such that

A65: pj = pj9 and

A66: j <= pj ;

reconsider pj9 = pj9 as Element of (N9 | j) by A63;

take pj = pj; :: thesis: S_{1}[j,pj]

N9 . pj = (N9 | j) . pj9 by A65, WAYBEL_9:16

.= the mapping of (N9 | j) . pj9 ;

hence S_{1}[j,pj]
by A62, A64, A66, XBOOLE_0:def 4; :: thesis: verum

end;not Bottom (BoolePoset ([#] L)) in F by A51, WAYBEL_7:4;

then A60: not {} in F by YELLOW_1:18;

G c= uparrow (fininfs G) by A22, A52;

then A61: G c= F by A50;

rng the mapping of (N9 | j) in G ;

then f0 /\ (rng the mapping of (N9 | j)) in F by A58, A61, WAYBEL_7:9;

then consider nj being Element of L such that

A62: nj in f0 /\ (rng the mapping of (N9 | j)) by A60, SUBSET_1:4;

nj in rng the mapping of (N9 | j) by A62, XBOOLE_0:def 4;

then consider pj9 being object such that

A63: pj9 in dom the mapping of (N9 | j) and

A64: nj = the mapping of (N9 | j) . pj9 by FUNCT_1:def 3;

pj9 in the carrier of (N9 | j) by A63;

then pj9 in { y9 where y9 is Element of N9 : j <= y9 } by WAYBEL_9:12;

then consider pj being Element of N9 such that

A65: pj = pj9 and

A66: j <= pj ;

reconsider pj9 = pj9 as Element of (N9 | j) by A63;

take pj = pj; :: thesis: S

N9 . pj = (N9 | j) . pj9 by A65, WAYBEL_9:16

.= the mapping of (N9 | j) . pj9 ;

hence S

A67: for j being Element of N9 holds S

for b being object st b in rng the mapping of (N9 * p) holds

b in f0

proof

then
rng the mapping of (N9 * p) c= f0
;
let b be object ; :: thesis: ( b in rng the mapping of (N9 * p) implies b in f0 )

assume b in rng the mapping of (N9 * p) ; :: thesis: b in f0

then b in { ((N9 * p) . k) where k is Element of (N9 * p) : verum } by WAYBEL11:19;

then consider k being Element of (N9 * p) such that

A68: b = (N9 * p) . k ;

reconsider l = k as Element of N9 by WAYBEL28:6;

the carrier of (N9 * p) = the carrier of N9 by WAYBEL28:6;

then k in the carrier of N9 ;

then A69: k in dom p by FUNCT_2:52;

(N9 * p) . k = ( the mapping of N9 * p) . k by WAYBEL28:def 2

.= N9 . (p . l) by A69, FUNCT_1:13 ;

hence b in f0 by A67, A68; :: thesis: verum

end;assume b in rng the mapping of (N9 * p) ; :: thesis: b in f0

then b in { ((N9 * p) . k) where k is Element of (N9 * p) : verum } by WAYBEL11:19;

then consider k being Element of (N9 * p) such that

A68: b = (N9 * p) . k ;

reconsider l = k as Element of N9 by WAYBEL28:6;

the carrier of (N9 * p) = the carrier of N9 by WAYBEL28:6;

then k in the carrier of N9 ;

then A69: k in dom p by FUNCT_2:52;

(N9 * p) . k = ( the mapping of N9 * p) . k by WAYBEL28:def 2

.= N9 . (p . l) by A69, FUNCT_1:13 ;

hence b in f0 by A67, A68; :: thesis: verum

then A70: "/\" (f0,L) <= "/\" ((rng the mapping of (N9 * p)),L) by WAYBEL_7:1;

A71: for M being subnet of N9 st M in NetUniv L holds

x >= inf M by A29, A56, WAYBEL28:3;

p is greater_or_equal_to_id by A67, WAYBEL28:def 1;

then A72: inf (N9 * p) <= x by A29, A27, A71, WAYBEL28:13;

inf (N9 * p) = Inf by WAYBEL_9:def 2

.= "/\" ((rng the mapping of (N9 * p)),L) by YELLOW_2:def 6 ;

hence y <= x by A57, A72, A70, YELLOW_0:def 2; :: thesis: verum

( ex_sup_of { (inf f) where f is Subset of L : f in F } ,L & ex_sup_of { (inf (N9 | j)) where j is Element of N9 : verum } ,L ) by YELLOW_0:17;

then x <= lim_inf F by A28, A53, YELLOW_0:34;

then x = lim_inf F by A73, YELLOW_0:def 3;

hence contradiction by A14, A50, A51, A26, A15; :: thesis: verum

then A ` is open by A2;

hence A is closed ; :: thesis: verum