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

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

set j = the Element of N;

A1: { (N . i) where i is Element of N : i >= the Element of N } c= rng the mapping of N

set x = "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L);

( ex_inf_of { (N . i) where i is Element of N : i >= the Element of N } ,L & ex_inf_of rng the mapping of N,L ) by YELLOW_0:17;

then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) >= "/\" ((rng the mapping of N),L) by A1, YELLOW_0:35;

then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) >= Inf by YELLOW_2:def 6;

then A4: inf N <= "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) by WAYBEL_9:def 2;

ex_sup_of X,L by YELLOW_0:17;

then ( "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) in X & X is_<=_than "\/" (X,L) ) by YELLOW_0:def 9;

then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) <= "\/" (X,L) by LATTICE3:def 9;

hence inf N <= lim_inf N by A4, YELLOW_0:def 2; :: thesis: verum

let N be net of L; :: thesis: inf N <= lim_inf N

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

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 ;
let x be object ; :: 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 ex j1 being Element of N st x = "/\" ( { (N . i) where i is Element of N : i >= j1 } ,L) ;

hence x in the carrier of L ; :: thesis: verum

end;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 ex j1 being Element of N st x = "/\" ( { (N . i) where i is Element of N : i >= j1 } ,L) ;

hence x in the carrier of L ; :: thesis: verum

set j = the Element of N;

A1: { (N . i) where i is Element of N : i >= the Element of N } c= rng the mapping of N

proof

reconsider X = X as Subset of L ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (N . i) where i is Element of N : i >= the Element of N } or x in rng the mapping of N )

A2: dom the mapping of N = the carrier of N by FUNCT_2:def 1;

assume x in { (N . i) where i is Element of N : i >= the Element of N } ; :: thesis: x in rng the mapping of N

then consider i being Element of N such that

A3: x = N . i and

i >= the Element of N ;

x = the mapping of N . i by A3, WAYBEL_0:def 8;

hence x in rng the mapping of N by A2, FUNCT_1:def 3; :: thesis: verum

end;A2: dom the mapping of N = the carrier of N by FUNCT_2:def 1;

assume x in { (N . i) where i is Element of N : i >= the Element of N } ; :: thesis: x in rng the mapping of N

then consider i being Element of N such that

A3: x = N . i and

i >= the Element of N ;

x = the mapping of N . i by A3, WAYBEL_0:def 8;

hence x in rng the mapping of N by A2, FUNCT_1:def 3; :: thesis: verum

set x = "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L);

( ex_inf_of { (N . i) where i is Element of N : i >= the Element of N } ,L & ex_inf_of rng the mapping of N,L ) by YELLOW_0:17;

then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) >= "/\" ((rng the mapping of N),L) by A1, YELLOW_0:35;

then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) >= Inf by YELLOW_2:def 6;

then A4: inf N <= "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) by WAYBEL_9:def 2;

ex_sup_of X,L by YELLOW_0:17;

then ( "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) in X & X is_<=_than "\/" (X,L) ) by YELLOW_0:def 9;

then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) <= "\/" (X,L) by LATTICE3:def 9;

hence inf N <= lim_inf N by A4, YELLOW_0:def 2; :: thesis: verum