let S, T be non empty Poset; :: thesis: for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is directed-sups-preserving
let f be Function of S,T; :: thesis: ( ( for X being Ideal of S holds f preserves_sup_of X ) implies f is directed-sups-preserving )
assume A1: for X being Ideal of S holds f preserves_sup_of X ; :: thesis: f is directed-sups-preserving
let X be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( not X is empty & X is directed implies f preserves_sup_of X )
assume that
A2: ( not X is empty & X is directed ) and
A3: ex_sup_of X,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) )
reconsider Y = X as non empty directed Subset of S by A2;
downarrow Y is Ideal of S ;
then ( f preserves_sup_of downarrow X & ex_sup_of downarrow X,S ) by A1, A3, Th32;
then A4: ( ex_sup_of f .: (downarrow X),T & sup (f .: (downarrow X)) = f . (sup (downarrow X)) & sup (downarrow X) = sup X ) by A3, Def31, Th33;
X c= downarrow X by Th16;
then A5: f .: X c= f .: (downarrow X) by RELAT_1:156;
A6: f .: (downarrow X) is_<=_than f . (sup X) by A4, YELLOW_0:30;
A7: f .: X is_<=_than f . (sup X)

proof

let x be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not x in f .: X or x <= f . (sup X) )
assume x in f .: X ; :: thesis: x <= f . (sup X)
hence x <= f . (sup X) by A5, A6, LATTICE3:def 9; :: thesis: verum

end;

A8: now

let b be Element of T; :: thesis: ( f .: X is_<=_than b implies f . (sup X) <= b )
assume A9: f .: X is_<=_than b ; :: thesis: f . (sup X) <= b
f .: (downarrow X) is_<=_than b

proof

let a be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not a in f .: (downarrow X) or a <= b )
assume a in f .: (downarrow X) ; :: thesis: a <= b
then consider x being set such that
A10: ( x in dom f & x in downarrow X & a = f . x ) by FUNCT_1:def 12;
downarrow X = { z where z is Element of S : ex y being Element of S st
( z <= y & y in X ) } by Th14;
then consider z being Element of S such that
A11: ( x = z & ex y being Element of S st
( z <= y & y in X ) ) by A10;
consider y being Element of S such that
A12: ( z <= y & y in X ) by A11;
( f is monotone & f . y in f .: X ) by A1, A12, Th72, FUNCT_2:43;
then ( f . z <= f . y & f . y <= b ) by A9, A12, LATTICE3:def 9, ORDERS_3:def 5;
hence a <= b by A10, A11, ORDERS_2:26; :: thesis: verum

end;

hence f . (sup X) <= b by A4, YELLOW_0:30; :: thesis: verum

end;

hence ex_sup_of f .: X,T by A7, YELLOW_0:15; :: thesis: sup (f .: X) = f . (sup X)
hence sup (f .: X) = f . (sup X) by A7, A8, YELLOW_0:def 9; :: thesis: verum