let R be up-complete LATTICE; :: thesis: for N being reflexive monotone net of R holds lim_inf N = sup N
let N be reflexive monotone net of R; :: thesis: lim_inf N = sup N
defpred S₁[ set ] means verum;
deffunc H₁( Element of N) -> Element of the carrier of R = N . $1;
deffunc H₂( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= $1 } ,R);
A1: for j being Element of N holds H₁(j) = H₂(j)

proof

let j be Element of N; :: thesis: H₁(j) = H₂(j)
set Y = { (N . i) where i is Element of N : i >= j } ;
A2: N . j is_<=_than { (N . i) where i is Element of N : i >= j }

proof

let y be Element of R; :: according to LATTICE3:def 8 :: thesis: ( not y in { (N . i) where i is Element of N : i >= j } or N . j <= y )
assume y in { (N . i) where i is Element of N : i >= j } ; :: thesis: N . j <= y
then ex i being Element of N st
( y = N . i & j <= i ) ;
hence N . j <= y by WAYBEL11:def 9; :: thesis: verum

end;

for b being Element of R st b is_<=_than { (N . i) where i is Element of N : i >= j } holds
N . j >= b

proof

let b be Element of R; :: thesis: ( b is_<=_than { (N . i) where i is Element of N : i >= j } implies N . j >= b )
assume A3: b is_<=_than { (N . i) where i is Element of N : i >= j } ; :: thesis: N . j >= b
reconsider j9 = j as Element of N ;
j9 <= j9 ;
then N . j9 in { (N . i) where i is Element of N : i >= j } ;
hence N . j >= b by A3; :: thesis: verum

end;

hence H₁(j) = H₂(j) by A2, YELLOW_0:31; :: thesis: verum

end;

rng the mapping of N = { H₁(j) where j is Element of N : S₁[j] } by WAYBEL11:19
.= { H₂(j) where j is Element of N : S₁[j] } from FRAENKEL:sch 5(A1) ;
hence lim_inf N = Sup by YELLOW_2:def 5
.= sup N by WAYBEL_2:def 1 ;
:: thesis: verum