let R be up-complete /\-complete LATTICE; :: thesis: for N being net of R holds sup (inf_net N) = lim_inf N
let N be net of R; :: thesis: sup (inf_net N) = lim_inf N
defpred S₁[ set ] means verum;
deffunc H₁( Element of N) -> Element of the carrier of R = "/\" ( { (N . l) where l is Element of N : l >= $1 } ,R);
sup (inf_net N) = Sup by WAYBEL_2:def 1
.= sup (rng the mapping of (inf_net N)) by YELLOW_2:def 5
.= lim_inf N by Th23 ;
hence sup (inf_net N) = lim_inf N ; :: thesis: verum