let S, T be non empty up-complete Poset; :: thesis: for f being monotone Function of S,T
for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D)
let f be monotone Function of S,T; :: thesis: for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D)
let X be non empty directed Subset of S; :: thesis: lim_inf (f * (Net-Str X)) = sup (f .: X)
set M = Net-Str X;
set N = f * (Net-Str X);
deffunc H₁( Element of (f * (Net-Str X))) -> set = { ((f * (Net-Str X)) . i) where i is Element of (f * (Net-Str X)) : i >= $1 } ;
deffunc H₂( Element of (f * (Net-Str X))) -> Element of the carrier of T = "/\" H₁($1),T;
set NT = { H₂(j) where j is Element of (f * (Net-Str X)) : verum } ;
A1: ( RelStr(# the carrier of (f * (Net-Str X)),the InternalRel of (f * (Net-Str X)) #) = RelStr(# the carrier of (Net-Str X),the InternalRel of (Net-Str X) #) & the mapping of (f * (Net-Str X)) = f * the mapping of (Net-Str X) ) by WAYBEL_9:def 8;
A2: ( the carrier of (Net-Str X) = X & the mapping of (Net-Str X) = id X ) by Th32;

A3: now

let i be Element of (f * (Net-Str X)); :: thesis: (f * (Net-Str X)) . i = f . i
thus (f * (Net-Str X)) . i = f . ((id X) . i) by A1, A2, FUNCT_2:21
.= f . i by A1, A2, FUNCT_1:35 ; :: thesis: verum

end;

A4: for i being Element of (f * (Net-Str X)) holds H₂(i) = f . i

proof

let i be Element of (f * (Net-Str X)); :: thesis: H₂(i) = f . i
i in X by A1, A2;
then reconsider x = i as Element of S ;
A5: i <= i ;
(f * (Net-Str X)) . i = f . x by A3;
then f . x in H₁(i) by A5;
then A6: for z being Element of T st z is_<=_than H₁(i) holds
z <= f . x by LATTICE3:def 8;
f . x is_<=_than H₁(i)

proof

let z be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not z in H₁(i) or f . x <= z )
assume z in H₁(i) ; :: thesis: f . x <= z
then consider j being Element of (f * (Net-Str X)) such that
A7: ( z = (f * (Net-Str X)) . j & j >= i ) ;
reconsider j = j as Element of (f * (Net-Str X)) ;
j in X by A1, A2;
then reconsider y = j as Element of S ;
( Net-Str X is full SubRelStr of S & RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S,the InternalRel of S #) ) by Th32;
then f * (Net-Str X) is full SubRelStr of S by A1, Th12;
then y >= x by A7, YELLOW_0:60;
then f . y >= f . x by WAYBEL_1:def 2;
hence f . x <= z by A3, A7; :: thesis: verum

end;

hence H₂(i) = f . i by A6, YELLOW_0:31; :: thesis: verum

end;

{ H₂(j) where j is Element of (f * (Net-Str X)) : verum } = f .: X

proof

thus { H₂(j) where j is Element of (f * (Net-Str X)) : verum } c= f .: X :: according to XBOOLE_0:def 10 :: thesis: f .: X c= { H₂(j) where j is Element of (f * (Net-Str X)) : verum }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₂(j) where j is Element of (f * (Net-Str X)) : verum } or x in f .: X )
assume x in { H₂(j) where j is Element of (f * (Net-Str X)) : verum } ; :: thesis: x in f .: X
then consider j being Element of (f * (Net-Str X)) such that
A8: x = H₂(j) ;
reconsider j = j as Element of (f * (Net-Str X)) ;
( x = f . j & j in X & the carrier of T <> {} ) by A1, A2, A4, A8;
hence x in f .: X by FUNCT_2:43; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: X or y in { H₂(j) where j is Element of (f * (Net-Str X)) : verum } )
assume y in f .: X ; :: thesis: y in { H₂(j) where j is Element of (f * (Net-Str X)) : verum }
then consider x being set such that
A9: ( x in the carrier of S & x in X & y = f . x ) by FUNCT_2:115;
reconsider x = x as Element of S by A9;
reconsider i = x as Element of (f * (Net-Str X)) by A1, A9, Th32;
f . x = H₂(i) by A4;
hence y in { H₂(j) where j is Element of (f * (Net-Str X)) : verum } by A9; :: thesis: verum

end;

hence lim_inf (f * (Net-Str X)) = sup (f .: X) by WAYBEL11:def 6; :: thesis: verum