let L be complete LATTICE; :: thesis: for N being net of L holds inf N <= lim_inf N
let N be net of L; :: thesis: inf N <= lim_inf N
consider j being Element of N;
A1: ( ex_inf_of { (N . i) where i is Element of N : i >= j } ,L & ex_inf_of rng the mapping of N,L ) by YELLOW_0:17;
{ (N . i) where i is Element of N : i >= j } c= rng the mapping of N

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (N . i) where i is Element of N : i >= j } or x in rng the mapping of N )
assume x in { (N . i) where i is Element of N : i >= j } ; :: thesis: x in rng the mapping of N
then consider i being Element of N such that
A2: x = N . i and
i >= j ;
A3: x = the mapping of N . i by A2, WAYBEL_0:def 8;
dom the mapping of N = the carrier of N by FUNCT_2:def 1;
hence x in rng the mapping of N by A3, FUNCT_1:def 5; :: thesis: verum

end;

then A4: "/\" { (N . i) where i is Element of N : i >= j } ,L >= "/\" (rng the mapping of N),L by A1, YELLOW_0:35;
set x = "/\" { (N . i) where i is Element of N : i >= j } ,L;
"/\" { (N . i) where i is Element of N : i >= j } ,L >= Inf by A4, YELLOW_2:def 6;
then A5: inf N <= "/\" { (N . i) where i is Element of N : i >= j } ,L by WAYBEL_9:def 2;
set X = { ("/\" { (N . i) where i is Element of N : i >= j1 } ,L) where j1 is Element of N : verum } ;
{ ("/\" { (N . i) where i is Element of N : i >= j1 } ,L) where j1 is Element of N : verum } c= the carrier of L

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("/\" { (N . i) where i is Element of N : i >= j1 } ,L) where j1 is Element of N : verum } or x in the carrier of L )
assume x in { ("/\" { (N . i) where i is Element of N : i >= j1 } ,L) where j1 is Element of N : verum } ; :: thesis: x in the carrier of L
then consider j1 being Element of N such that
A6: x = "/\" { (N . i) where i is Element of N : i >= j1 } ,L ;
thus x in the carrier of L by A6; :: thesis: verum

end;

then reconsider X = { ("/\" { (N . i) where i is Element of N : i >= j1 } ,L) where j1 is Element of N : verum } as Subset of L ;
reconsider X = X as Subset of L ;
A7: "/\" { (N . i) where i is Element of N : i >= j } ,L in X ;
ex_sup_of X,L by YELLOW_0:17;
then X is_<=_than "\/" X,L by YELLOW_0:def 9;
then "/\" { (N . i) where i is Element of N : i >= j } ,L <= "\/" X,L by A7, LATTICE3:def 9;
hence inf N <= lim_inf N by A5, YELLOW_0:def 2; :: thesis: verum