let L be complete LATTICE; :: thesis: for D being non empty directed Subset of L
for M being subnet of Net-Str D holds lim_inf M = sup D

let D be non empty directed Subset of L; :: thesis: for M being subnet of Net-Str D holds lim_inf M = sup D
for M being subnet of Net-Str D holds sup D >= inf M
proof
let M be subnet of Net-Str D; :: thesis: sup D >= inf M
set i = the Element of M;
set f = the mapping of M;
consider g being Function of M,() such that
A1: the mapping of M = the mapping of () * g and
for m being Element of () ex n being Element of M st
for p being Element of M st n <= p holds
m <= g . p by YELLOW_6:def 9;
A2: dom the mapping of M = the carrier of M by FUNCT_2:def 1;
then the mapping of M . the Element of M in rng the mapping of M by FUNCT_1:def 3;
then A3: "/\" ((rng the mapping of M),L) <= the mapping of M . the Element of M by ;
g . the Element of M in the carrier of () ;
then A4: g . the Element of M in D by WAYBEL21:32;
then g . the Element of M = (id D) . (g . the Element of M) by FUNCT_1:18
.= the mapping of () . (g . the Element of M) by WAYBEL21:32
.= the mapping of M . the Element of M by ;
then the mapping of M . the Element of M <= sup D by ;
then sup D >= "/\" ((rng the mapping of M),L) by ;
then sup D >= Inf by YELLOW_2:def 6;
hence sup D >= inf M by WAYBEL_9:def 2; :: thesis: verum
end;
then ( lim_inf () = sup D & ( for p being greater_or_equal_to_id Function of (),() holds sup D >= inf (() * p) ) ) by WAYBEL17:10;
hence for M being subnet of Net-Str D holds lim_inf M = sup D by Th14; :: thesis: verum