let R be /\-complete Semilattice; :: 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
deffunc H₁( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= $1 } ,R);
deffunc H₂( Element of N) -> Element of the carrier of R = N . $1;
defpred S₁[ set ] means verum;
set X = { H₁(j) where j is Element of N : S₁[j] } ;
A1: for j being Element of N holds H₂(j) = H₁(j)

proof

let j be Element of N; :: thesis: H₂(j) = H₁(j)
defpred S₂[ Element of N] means $1 >= j;
set Y = { H₂(i) where i is Element of N : S₂[i] } ;
j <= j ;
then A2: N . j in { H₂(i) where i is Element of N : S₂[i] } ;
{ H₂(i) where i is Element of N : S₂[i] } is Subset of R from DOMAIN_1:sch 8();
then A3: ex_inf_of { H₂(i) where i is Element of N : S₂[i] } ,R by A2, WAYBEL_0:76;
A4: N . j is_<=_than { H₂(i) where i is Element of N : S₂[i] }

proof

let y be Element of R; :: according to LATTICE3:def 8 :: thesis: ( not y in { H₂(i) where i is Element of N : S₂[i] } or N . j <= y )
assume y in { H₂(i) where i is Element of N : S₂[i] } ; :: 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 { H₂(i) where i is Element of N : S₂[i] } holds
N . j >= b

proof

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

end;

hence H₂(j) = H₁(j) by A3, A4, YELLOW_0:def 10; :: 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