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,(Net-Str D) such that
A1: the mapping of M = the mapping of (Net-Str D) * g and
for m being Element of (Net-Str D) 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 YELLOW_0:17, YELLOW_4:2;
g . the Element of M in the carrier of (Net-Str D) ;
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 (Net-Str D) . (g . the Element of M) by WAYBEL21:32
.= the mapping of M . the Element of M by A1, A2, FUNCT_1:12 ;
then the mapping of M . the Element of M <= sup D by A4, YELLOW_2:22;
then sup D >= "/\" ((rng the mapping of M),L) by A3, YELLOW_0:def 2;
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 (Net-Str D) = sup D & ( for p being greater_or_equal_to_id Function of (Net-Str D),(Net-Str D) holds sup D >= inf ((Net-Str D) * p) ) ) by WAYBEL17:10;
hence for M being subnet of Net-Str D holds lim_inf M = sup D by Th14; :: thesis: verum