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

b <= x

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

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

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
let k0 be Element of M; :: thesis: "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= x

defpred S_{1}[ 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 ) ) )

ex u being object st

( u in the carrier of M & S_{1}[e,u] )

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

reconsider p = f * g as Function of N,N ;

for j being Element of N holds j <= p . j

A21: { ((N * p) . j) where j is Element of (N * p) : verum } c= { (M . k) where k is Element of M : k >= k0 }

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 }

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;defpred S

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

A11:
for e being object st e in the carrier of N holds
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;( 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

ex u being object st

( u in the carrier of M & S

proof

consider g being Function such that
let e be object ; :: thesis: ( e in the carrier of N implies ex u being object st

( u in the carrier of M & S_{1}[e,u] ) )

assume e in the carrier of N ; :: thesis: ex u being object st

( u in the carrier of M & S_{1}[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_{1}[e,u] )

thus u in the carrier of M ; :: thesis: S_{1}[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;( u in the carrier of M & S

assume e in the carrier of N ; :: thesis: ex u being object st

( u in the carrier of M & S

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

thus u in the carrier of M ; :: thesis: S

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

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

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

reconsider g = g as Function of N,M ;
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 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

reconsider p = f * g as Function of N,N ;

for j being Element of N holds j <= p . j

proof

then reconsider p = p as greater_or_equal_to_id Function of N,N by Def1;
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;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

A21: { ((N * p) . j) where j is Element of (N * p) : verum } c= { (M . k) where k is Element of M : k >= k0 }

proof

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

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

A31:
inf (N * p) <= x
by A2;
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)

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;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 rng the mapping of (N * p) )
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;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

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

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

b <= x

proof

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

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