let L be non empty complete LATTICE; :: thesis: for D being non empty directed Subset of L holds [(Net-Str D),(sup D)] in lim_inf-Convergence L
let D be non empty directed Subset of L; :: thesis: [(Net-Str D),(sup D)] in lim_inf-Convergence L
( Net-Str D in NetUniv L & ( for M being subnet of Net-Str D holds lim_inf M = sup D ) ) by Th24, Th25;
hence [(Net-Str D),(sup D)] in lim_inf-Convergence L by Def3; :: thesis: verum