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 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 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 ;
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:
( ( for M being subnet of a_net F holds lim_inf F = lim_inf M ) & a_net F in NetUniv L ) by ;
then A5: [(),()] 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 () such that
A6: for j being Element of () st i <= j holds
() . j in A ` ;
A7: the carrier of () = { [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 () ;
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 ;
set b = the Element of B;
not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;
then not B is empty by ;
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 () by A7, A9, A12;
then reconsider j = [ the Element of B,B] as Element of () ;
B c= f by ;
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 ;
hence contradiction by A12, A13, XBOOLE_0:def 5; :: thesis: verum
end;
assume A14: for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
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 `
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:
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= [:(), the carrier of L:] by YELLOW_6:def 18;
then A19: N in NetUniv L by ;
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
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;
then reconsider G = { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } as non empty Subset of (BoolePoset ([#] L)) by ;
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
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 ;
then A25: q in dom the mapping of N9 by XBOOLE_0:def 4;
p = the mapping of N9 . q by ;
hence p in rng the mapping of N9 by ; :: thesis: verum
end;
then rj c= rng the mapping of N9 ;
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 () by ;
A27: x = lim_inf N9 by ;
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 ;
then the carrier of N9 in the_universe_of the carrier of L by ;
then A29: N9 in NetUniv L by YELLOW_6:def 11;
A30: not {} in fininfs G
proof
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 S1[ 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 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in Y implies ex y being object st
( y in the carrier of N9 & S1[x,y] ) )

assume x in Y ; :: thesis: ex y being object st
( y in the carrier of N9 & S1[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 S1[x,y] ; :: thesis: contradiction
hence contradiction by A34; :: thesis: verum
end;
consider f being Function such that
A35: ( dom f = Y & rng f c= the carrier of N9 ) and
A36: for x being object st x in Y holds
S1[x,f . x] from reconsider C = rng f as finite Subset of ([#] N9) by ;
[#] 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
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 ;
A41: f . y in rng f by ;
then reconsider f1 = f . y as Element of N9 by A35;
A42: f1 <= j0 by ;
for p being object st p in rng the mapping of (N9 | j0) holds
p in y
proof
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 ;
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 ;
then q in { m9 where m9 is Element of N9 : j1 <= m9 } by ;
then A48: q in the carrier of (N9 | j1) by WAYBEL_9:12;
q in dom the mapping of N9 by ;
then q in (dom the mapping of N9) /\ the carrier of (N9 | j1) by ;
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 ;
then p = ( the mapping of N9 | the carrier of (N9 | j1)) . q by ;
then p in rng ( the mapping of N9 | the carrier of (N9 | j1)) by ;
hence p in y by ; :: thesis: verum
end;
hence rng the mapping of (N9 | j0) c= y ; :: thesis: verum
end;
then rng the mapping of (N9 | j0) c= meet Y by ;
then rng the mapping of (N9 | j0) c= {} by ;
hence contradiction ; :: thesis: verum
end;
for y being Element of (BoolePoset ([#] L)) st Bottom (BoolePoset ([#] L)) >= y holds
not y in fininfs G
proof
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 ;
hence not y in fininfs G by A30; :: thesis: verum
end;
then not Bottom (BoolePoset ([#] L)) in uparrow () by WAYBEL_0:def 16;
then uparrow () is proper ;
then consider F being Filter of (BoolePoset ([#] L)) such that
A50: uparrow () c= F and
A51: F is ultra by WAYBEL_7:26;
A52: fininfs G c= uparrow () 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 ;
then A55: ( f1 in G & G c= F ) by A22;
x = Inf by
.= "/\" ((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;
now :: thesis: for M being subnet of N9 holds x = lim_inf M
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 ; :: thesis: verum
end;
then A56: for M being subnet of N9 st M in NetUniv L holds
x = lim_inf M ;
{ (inf f) where f is Subset of L : f in F } is_<=_than x
proof
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 S1[ Element of N9, Element of N9] means ( \$1 <= \$2 & N9 . \$2 in f0 );
A59: now :: thesis: for j being Element of N9 ex pj being Element of N9 st S1[j,pj]
let j be Element of N9; :: thesis: ex pj being Element of N9 st S1[j,pj]
not Bottom (BoolePoset ([#] L)) in F by ;
then A60: not {} in F by YELLOW_1:18;
G c= uparrow () by ;
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 ;
then consider nj being Element of L such that
A62: nj in f0 /\ (rng the mapping of (N9 | j)) by ;
nj in rng the mapping of (N9 | j) by ;
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: S1[j,pj]
N9 . pj = (N9 | j) . pj9 by
.= the mapping of (N9 | j) . pj9 ;
hence S1[j,pj] by A62, A64, A66, XBOOLE_0:def 4; :: thesis: verum
end;
consider p being Function of N9,N9 such that
A67: for j being Element of N9 holds S1[j,p . j] from for b being object st b in rng the mapping of (N9 * p) holds
b in f0
proof
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 ;
hence b in f0 by ; :: thesis: verum
end;
then rng the mapping of (N9 * p) c= 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 ;
p is greater_or_equal_to_id by ;
then A72: inf (N9 * p) <= x by ;
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 ; :: thesis: verum
end;
then A73: lim_inf F <= x by YELLOW_0:32;
( 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 ;
then x = lim_inf F by ;
hence contradiction by A14, A50, A51, A26, A15; :: thesis: verum
end;
then A ` in xi L by A1;
then A ` is open by A2;
hence A is closed ; :: thesis: verum