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
A1: Net-Str D in NetUniv L by Th25;
for M being subnet of Net-Str D holds lim_inf M = sup D by Th26;
hence [(Net-Str D),(sup D)] in lim_inf-Convergence L by A1, Def3; :: thesis: verum