let S, T be non empty RelStr ; :: thesis: for D being Subset of S
for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)

let D be Subset of S; :: thesis: for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)

let f be Function of S,T; :: thesis: ( ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone implies sup (f .: D) <= f . (sup D) )
assume A1: ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) ; :: thesis: ( not f is monotone or sup (f .: D) <= f . (sup D) )
A2: ex_sup_of D,S by ;
A3: ex_sup_of f .: D,T by ;
assume A4: f is monotone ; :: thesis: sup (f .: D) <= f . (sup D)
D is_<=_than sup D by ;
then f .: D is_<=_than f . (sup D) by ;
hence sup (f .: D) <= f . (sup D) by ; :: thesis: verum