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) #) by WAYBEL_9:def 8;
A2: the mapping of (f * (Net-Str X)) = f * the mapping of (Net-Str X) by WAYBEL_9:def 8;
A3: the carrier of (Net-Str X) = X by Th32;
A4: the mapping of (Net-Str X) = id X by Th32;

A5: now :: thesis: for i being Element of (f * (Net-Str X)) holds (f * (Net-Str X)) . i = f . i

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, A4, FUNCT_2:15
.= f . i by A1, A3 ; :: thesis: verum

end;

A6: 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, A3;
then reconsider x = i as Element of S ;
A7: i <= i ;
(f * (Net-Str X)) . i = f . x by A5;
then f . x in H₁(i) by A7;
then A8: for z being Element of T st z is_<=_than H₁(i) holds
z <= f . x ;
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
A9: z = (f * (Net-Str X)) . j and
A10: j >= i ;
reconsider j = j as Element of (f * (Net-Str X)) ;
j in X by A1, A3;
then reconsider y = j as Element of S ;
A11: Net-Str X is full SubRelStr of S by Th32;
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S, the InternalRel of S #) ;
then f * (Net-Str X) is full SubRelStr of S by A1, A11, Th12;
then y >= x by A10, YELLOW_0:59;
then f . y >= f . x by WAYBEL_1:def 2;
hence f . x <= z by A5, A9; :: thesis: verum

end;

hence H₂(i) = f . i by A8, 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 object ; :: 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
A12: x = H₂(j) ;
reconsider j = j as Element of (f * (Net-Str X)) ;
A13: x = f . j by A6, A12;
j in X by A1, A3;
hence x in f .: X by A13, FUNCT_2:35; :: thesis: verum

end;

let y be object ; :: 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 object such that
A14: x in the carrier of S and
A15: x in X and
A16: y = f . x by FUNCT_2:64;
reconsider x = x as Element of S by A14;
reconsider i = x as Element of (f * (Net-Str X)) by A1, A15, Th32;
f . x = H₂(i) by A6;
hence y in { H₂(j) where j is Element of (f * (Net-Str X)) : verum } by A16; :: thesis: verum

end;

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