let L be complete LATTICE; :: thesis: for N being net of L holds lim_inf N = "\/" { (inf (N | i)) where i is Element of N : verum } ,L
let N be net of L; :: thesis: lim_inf N = "\/" { (inf (N | i)) where i is Element of N : verum } ,L
set X = { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum } ;
set Y = { (inf (N | i)) where i is Element of N : verum } ;
A1: lim_inf N = "\/" { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum } ,L by WAYBEL11:def 6;
for x being set st x in { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum } holds
x in { (inf (N | i)) where i is Element of N : verum }

proof

let x be set ; :: thesis: ( x in { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum } implies x in { (inf (N | i)) where i is Element of N : verum } )
assume x in { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum } ; :: thesis: x in { (inf (N | i)) where i is Element of N : verum }
then consider j being Element of N such that
A2: x = "/\" { (N . i) where i is Element of N : i >= j } ,L ;
set S = { (N . i) where i is Element of N : i >= j } ;
reconsider x = x as Element of L by A2;
A3: ex_inf_of { (N . i) where i is Element of N : i >= j } ,L by YELLOW_0:17;
then A4: ( { (N . i) where i is Element of N : i >= j } is_>=_than x & ( for a being Element of L st { (N . i) where i is Element of N : i >= j } is_>=_than a holds
a <= x ) ) by A2, YELLOW_0:def 10;
reconsider i = j as Element of N ;
A5: ex_inf_of rng the mapping of (N | i),L by YELLOW_0:17;
for b being set st b in rng the mapping of (N | i) holds
b in { (N . i) where i is Element of N : i >= j }

proof

let b be set ; :: thesis: ( b in rng the mapping of (N | i) implies b in { (N . i) where i is Element of N : i >= j } )
assume b in rng the mapping of (N | i) ; :: thesis: b in { (N . i) where i is Element of N : i >= j }
then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;
then consider k being Element of (N | i) such that
A6: b = (N | i) . k ;
the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;
then reconsider l = k as Element of N by TARSKI:def 3;
k in the carrier of (N | i) ;
then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;
then consider y being Element of N such that
A7: ( k = y & i <= y ) ;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
hence b in { (N . i) where i is Element of N : i >= j } by A6, A7; :: thesis: verum

end;

then A8: rng the mapping of (N | i) c= { (N . i) where i is Element of N : i >= j } by TARSKI:def 3;
for b being set st b in { (N . i) where i is Element of N : i >= j } holds
b in rng the mapping of (N | i)

proof

let b be set ; :: thesis: ( b in { (N . i) where i is Element of N : i >= j } implies b in rng the mapping of (N | i) )
assume b in { (N . i) where i is Element of N : i >= j } ; :: thesis: b in rng the mapping of (N | i)
then consider k being Element of N such that
A9: ( b = N . k & k >= j ) ;
reconsider l = k as Element of N ;
l in { y where y is Element of N : i <= y } by A9;
then reconsider k = k as Element of (N | i) by WAYBEL_9:12;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A9;
hence b in rng the mapping of (N | i) by WAYBEL11:19; :: thesis: verum

end;

then { (N . i) where i is Element of N : i >= j } c= rng the mapping of (N | i) by TARSKI:def 3;
then A10: { (N . i) where i is Element of N : i >= j } = rng the mapping of (N | i) by A8, XBOOLE_0:def 10;
A11: rng the mapping of (N | i) is_>=_than x

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in rng the mapping of (N | i) or x <= b )
thus ( not b in rng the mapping of (N | i) or x <= b ) by A4, A8, LATTICE3:def 8; :: thesis: verum

end;

for a being Element of L st rng the mapping of (N | i) is_>=_than a holds
a <= x by A2, A3, A10, YELLOW_0:def 10;
then consider i being Element of N such that
A12: ( ex_inf_of rng the mapping of (N | i),L & rng the mapping of (N | i) is_>=_than x & ( for a being Element of L st rng the mapping of (N | i) is_>=_than a holds
a <= x ) ) by A5, A11;
A13: x = "/\" (rng the mapping of (N | i)),L by A12, YELLOW_0:def 10;
inf (N | i) = Inf by WAYBEL_9:def 2
.= "/\" (rng the mapping of (N | i)),L by YELLOW_2:def 6 ;
hence x in { (inf (N | i)) where i is Element of N : verum } by A13; :: thesis: verum

end;

then A14: { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum } c= { (inf (N | i)) where i is Element of N : verum } by TARSKI:def 3;
for x being set st x in { (inf (N | i)) where i is Element of N : verum } holds
x in { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum }

proof

let x be set ; :: thesis: ( x in { (inf (N | i)) where i is Element of N : verum } implies x in { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum } )
assume x in { (inf (N | i)) where i is Element of N : verum } ; :: thesis: x in { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum }
then consider i being Element of N such that
A15: x = inf (N | i) ;
reconsider x = x as Element of L by A15;
A16: x = Inf by A15, WAYBEL_9:def 2
.= "/\" (rng the mapping of (N | i)),L by YELLOW_2:def 6 ;
set S = { (N . j) where j is Element of N : j >= i } ;
rng the mapping of (N | i) = { (N . j) where j is Element of N : j >= i }

proof

for b being set st b in rng the mapping of (N | i) holds
b in { (N . j) where j is Element of N : j >= i }

proof

let b be set ; :: thesis: ( b in rng the mapping of (N | i) implies b in { (N . j) where j is Element of N : j >= i } )
assume b in rng the mapping of (N | i) ; :: thesis: b in { (N . j) where j is Element of N : j >= i }
then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;
then consider k being Element of (N | i) such that
A17: b = (N | i) . k ;
the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;
then reconsider l = k as Element of N by TARSKI:def 3;
k in the carrier of (N | i) ;
then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;
then consider y being Element of N such that
A18: ( k = y & i <= y ) ;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
hence b in { (N . j) where j is Element of N : j >= i } by A17, A18; :: thesis: verum

end;

then A19: rng the mapping of (N | i) c= { (N . j) where j is Element of N : j >= i } by TARSKI:def 3;
for b being set st b in { (N . j) where j is Element of N : j >= i } holds
b in rng the mapping of (N | i)

proof

let b be set ; :: thesis: ( b in { (N . j) where j is Element of N : j >= i } implies b in rng the mapping of (N | i) )
assume b in { (N . j) where j is Element of N : j >= i } ; :: thesis: b in rng the mapping of (N | i)
then consider k being Element of N such that
A20: ( b = N . k & k >= i ) ;
reconsider l = k as Element of N ;
l in { y where y is Element of N : i <= y } by A20;
then reconsider k = k as Element of (N | i) by WAYBEL_9:12;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A20;
hence b in rng the mapping of (N | i) by WAYBEL11:19; :: thesis: verum

end;

then { (N . j) where j is Element of N : j >= i } c= rng the mapping of (N | i) by TARSKI:def 3;
hence rng the mapping of (N | i) = { (N . j) where j is Element of N : j >= i } by A19, XBOOLE_0:def 10; :: thesis: verum

end;

hence x in { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum } by A16; :: thesis: verum

end;

then { (inf (N | i)) where i is Element of N : verum } c= { ("/\" { (N . i) where i is Element of N : i >= j } ,L) where j is Element of N : verum } by TARSKI:def 3;
hence lim_inf N = "\/" { (inf (N | i)) where i is Element of N : verum } ,L by A1, A14, XBOOLE_0:def 10; :: thesis: verum