let S be up-complete LATTICE; :: thesis: for D being non empty directed Subset of S holds lim_inf (Net-Str D) = sup D
let D be non empty directed Subset of S; :: thesis: lim_inf (Net-Str D) = sup D
set F = (id the carrier of S) | D;
A1: (id the carrier of S) | D = id D by FUNCT_3:1;
lim_inf (Net-Str D) = sup (Net-Str D) by Lm6
.= Sup by WAYBEL_2:def 1
.= "\/" ((rng ((id the carrier of S) | D)),S) by YELLOW_2:def 5
.= sup D by A1, RELAT_1:45 ;
hence lim_inf (Net-Str D) = sup D ; :: thesis: verum