let R be up-complete /\-complete LATTICE; :: thesis: for N being net of R
for i being Element of N holds sup (inf_net N) = lim_inf (N | i)
let N be net of R; :: thesis: for i being Element of N holds sup (inf_net N) = lim_inf (N | i)
let i be Element of N; :: thesis: sup (inf_net N) = lim_inf (N | i)
sup (inf_net N) = lim_inf N by Th24;
hence sup (inf_net N) = lim_inf (N | i) by WAYBEL21:41; :: thesis: verum