let L be complete LATTICE; :: thesis: for N being net of L
for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds
for M being subnet of N holds x = lim_inf M
let N be net of L; :: thesis: for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds
for M being subnet of N holds x = lim_inf M
let x be Element of L; :: thesis: ( x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) implies for M being subnet of N holds x = lim_inf M )
assume that
A1: x = lim_inf N and
A2: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ; :: thesis: for M being subnet of N holds x = lim_inf M
let M be subnet of N; :: thesis: x = lim_inf M
consider f being Function of M,N such that
A3: the mapping of M = the mapping of N * f and
A4: for j being Element of N ex k being Element of M st
for m being Element of M st k <= m holds
j <= f . m by YELLOW_6:def 9;
A5: x <= lim_inf M by A1, WAYBEL21:37;
A6: for k0 being Element of M holds "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= x

proof

let k0 be Element of M; :: thesis: "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= x
defpred S₁[ object , object ] means for j being Element of N
for v, v9 being Element of M st $1 = j & $2 = v & v9 >= v holds
( v >= k0 & f . v9 >= j & f . v >= j );
A7: for j being Element of N ex v being Element of M st
( v >= k0 & ( for v9 being Element of M st v9 >= v holds
( f . v9 >= j & f . v >= j ) ) )

proof

let j be Element of N; :: thesis: ex v being Element of M st
( v >= k0 & ( for v9 being Element of M st v9 >= v holds
( f . v9 >= j & f . v >= j ) ) )
consider w being Element of M such that
A8: for w9 being Element of M st w <= w9 holds
j <= f . w9 by A4;
consider v being Element of M such that
A9: v >= k0 and
A10: v >= w by Th5;
take v ; :: thesis: ( v >= k0 & ( for v9 being Element of M st v9 >= v holds
( f . v9 >= j & f . v >= j ) ) )
thus v >= k0 by A9; :: thesis: for v9 being Element of M st v9 >= v holds
( f . v9 >= j & f . v >= j )
let v9 be Element of M; :: thesis: ( v9 >= v implies ( f . v9 >= j & f . v >= j ) )
assume v9 >= v ; :: thesis: ( f . v9 >= j & f . v >= j )
then v9 >= w by A10, YELLOW_0:def 2;
hence f . v9 >= j by A8; :: thesis: f . v >= j
thus f . v >= j by A8, A10; :: thesis: verum

end;

A11: for e being object st e in the carrier of N holds
ex u being object st
( u in the carrier of M & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in the carrier of N implies ex u being object st
( u in the carrier of M & S₁[e,u] ) )
assume e in the carrier of N ; :: thesis: ex u being object st
( u in the carrier of M & S₁[e,u] )
then reconsider e9 = e as Element of N ;
consider u being Element of M such that
A12: u >= k0 and
A13: for v9 being Element of M st v9 >= u holds
( f . v9 >= e9 & f . u >= e9 ) by A7;
take u ; :: thesis: ( u in the carrier of M & S₁[e,u] )
thus u in the carrier of M ; :: thesis: S₁[e,u]
let j be Element of N; :: thesis: for v, v9 being Element of M st e = j & u = v & v9 >= v holds
( v >= k0 & f . v9 >= j & f . v >= j )
let v, v9 be Element of M; :: thesis: ( e = j & u = v & v9 >= v implies ( v >= k0 & f . v9 >= j & f . v >= j ) )
assume that
A14: e = j and
A15: u = v and
A16: v9 >= v ; :: thesis: ( v >= k0 & f . v9 >= j & f . v >= j )
thus v >= k0 by A12, A15; :: thesis: ( f . v9 >= j & f . v >= j )
thus f . v9 >= j by A13, A14, A15, A16; :: thesis: f . v >= j
thus f . v >= j by A13, A14, A15, A16; :: thesis: verum

end;

consider g being Function such that
A17: dom g = the carrier of N and
A18: rng g c= the carrier of M and
A19: for e being object st e in the carrier of N holds
S₁[e,g . e] from FUNCT_1:sch 6(A11);
reconsider g = g as Function of the carrier of N, the carrier of M by A17, A18, FUNCT_2:2;
A20: for j being Element of N holds g . j >= k0

proof

let j be Element of N; :: thesis: g . j >= k0
reconsider v = g . j as Element of M ;
ex v9 being Element of M st
( v9 >= v & v9 >= v ) by Th5;
hence g . j >= k0 by A19; :: thesis: verum

end;

reconsider g = g as Function of N,M ;
reconsider p = f * g as Function of N,N ;
for j being Element of N holds j <= p . j

proof

let j be Element of N; :: thesis: j <= p . j
reconsider v = g . j as Element of M ;
[#] M is directed by WAYBEL_0:def 6;
then ex v9 being Element of M st
( v9 in [#] M & v <= v9 & v <= v9 ) by WAYBEL_0:def 1;
then j <= f . (g . j) by A19;
hence j <= p . j by A17, FUNCT_1:13; :: thesis: verum

end;

then reconsider p = p as greater_or_equal_to_id Function of N,N by Def1;
A21: { ((N * p) . j) where j is Element of (N * p) : verum } c= { (M . k) where k is Element of M : k >= k0 }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { ((N * p) . j) where j is Element of (N * p) : verum } or y in { (M . k) where k is Element of M : k >= k0 } )
assume y in { ((N * p) . j) where j is Element of (N * p) : verum } ; :: thesis: y in { (M . k) where k is Element of M : k >= k0 }
then consider j being Element of (N * p) such that
A22: y = (N * p) . j ;
reconsider j9 = j as Element of N by Th6;
A23: the carrier of (N * p) = the carrier of N by Th6;
y = the mapping of (N * p) . j by A22, WAYBEL_0:def 8
.= ( the mapping of N * (f * g)) . j by Def2
.= ( the mapping of M * g) . j by A3, RELAT_1:36
.= the mapping of M . (g . j) by A17, A23, FUNCT_1:13 ;
then A24: y = M . (g . j9) by WAYBEL_0:def 8;
g . j9 >= k0 by A20;
hence y in { (M . k) where k is Element of M : k >= k0 } by A24; :: thesis: verum

end;

A25: ( ex_inf_of { ((N * p) . j) where j is Element of (N * p) : verum } ,L & ex_inf_of { (M . k) where k is Element of M : k >= k0 } ,L ) by YELLOW_0:17;
A26: dom the mapping of (N * p) = the carrier of (N * p) by FUNCT_2:def 1;
A27: rng the mapping of (N * p) = { ((N * p) . j) where j is Element of (N * p) : verum }

proof

thus rng the mapping of (N * p) c= { ((N * p) . j) where j is Element of (N * p) : verum } :: according to XBOOLE_0:def 10 :: thesis: { ((N * p) . j) where j is Element of (N * p) : verum } c= rng the mapping of (N * p)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng the mapping of (N * p) or y in { ((N * p) . j) where j is Element of (N * p) : verum } )
assume y in rng the mapping of (N * p) ; :: thesis: y in { ((N * p) . j) where j is Element of (N * p) : verum }
then consider j1 being object such that
A28: j1 in dom the mapping of (N * p) and
A29: the mapping of (N * p) . j1 = y by FUNCT_1:def 3;
reconsider j1 = j1 as Element of (N * p) by A28;
y = (N * p) . j1 by A29, WAYBEL_0:def 8;
hence y in { ((N * p) . j) where j is Element of (N * p) : verum } ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { ((N * p) . j) where j is Element of (N * p) : verum } or y in rng the mapping of (N * p) )
assume y in { ((N * p) . j) where j is Element of (N * p) : verum } ; :: thesis: y in rng the mapping of (N * p)
then consider j being Element of (N * p) such that
A30: y = (N * p) . j ;
y = the mapping of (N * p) . j by A30, WAYBEL_0:def 8;
hence y in rng the mapping of (N * p) by A26, FUNCT_1:def 3; :: thesis: verum

end;

A31: inf (N * p) <= x by A2;
inf (N * p) = Inf by WAYBEL_9:def 2
.= "/\" ( { ((N * p) . j) where j is Element of (N * p) : verum } ,L) by A27, YELLOW_2:def 6 ;
then "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= inf (N * p) by A25, A21, YELLOW_0:35;
hence "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= x by A31, YELLOW_0:def 2; :: thesis: verum

end;

for b being Element of L st b in { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } holds
b <= x

proof

let b be Element of L; :: thesis: ( b in { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } implies b <= x )
assume b in { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } ; :: thesis: b <= x
then ex k0 being Element of M st b = "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) ;
hence b <= x by A6; :: thesis: verum

end;

then A32: x is_>=_than { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } by LATTICE3:def 9;
ex_sup_of { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } ,L by YELLOW_0:17;
then "\/" ( { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } ,L) <= x by A32, YELLOW_0:def 9;
hence x = lim_inf M by A5, ORDERS_2:2; :: thesis: verum