let S, T be complete LATTICE; :: thesis: for f being Function of S,T st ( for N being net of S holds f . () <= lim_inf (f * N) ) holds
f is directed-sups-preserving

let f be Function of S,T; :: thesis: ( ( for N being net of S holds f . () <= lim_inf (f * N) ) implies f is directed-sups-preserving )
assume A1: for N being net of S holds f . () <= lim_inf (f * N) ; :: thesis:
thus f is directed-sups-preserving :: thesis: verum
proof
let D be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or f preserves_sup_of D )
assume ( not D is empty & D is directed ) ; :: thesis:
then reconsider D = D as non empty directed Subset of S ;
A2: f is monotone by ;
then A3: sup (f .: D) <= f . (sup D) by Th15;
A4: f . (sup D) <= sup (f .: D)
proof
sup D = lim_inf () by Th10;
then A5: f . (sup D) <= lim_inf (f * ()) by A1;
reconsider fN = f * () as reflexive monotone net of T by A2;
A6: sup fN = Sup by WAYBEL_2:def 1
.= Sup by WAYBEL_9:def 8
.= sup (rng (f * ((id the carrier of S) | D))) by YELLOW_2:def 5 ;
rng (f * ((id the carrier of S) | D)) = rng (f * (id D)) by FUNCT_3:1
.= rng (f | D) by RELAT_1:65
.= f .: D by RELAT_1:115 ;
hence f . (sup D) <= sup (f .: D) by ; :: thesis: verum
end;
f preserves_sup_of D by ;
hence f preserves_sup_of D ; :: thesis: verum
end;