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

hence for M being subnet of Net-Str D holds lim_inf M = sup D by Th14; :: thesis: verum

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

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;
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;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

hence for M being subnet of Net-Str D holds lim_inf M = sup D by Th14; :: thesis: verum