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