let S, T be non empty reflexive antisymmetric RelStr ; :: thesis: for D being non empty directed 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 up-complete & T is up-complete ) ) & f is monotone holds

sup (f .: D) <= f . (sup D)

let D be non empty directed 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 up-complete & T is up-complete ) ) & 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 up-complete & T is up-complete ) ) & 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 up-complete & T is up-complete ) ) ; :: thesis: ( not f is monotone or sup (f .: D) <= f . (sup D) )

assume A2: f is monotone ; :: thesis: sup (f .: D) <= f . (sup D)

then reconsider fD = f .: D as non empty directed Subset of T by YELLOW_2:15;

A3: ex_sup_of fD,T by A1, WAYBEL_0:75;

ex_sup_of D,S by A1, WAYBEL_0:75;

then D is_<=_than sup D by YELLOW_0:30;

then f .: D is_<=_than f . (sup D) by A2, YELLOW_2:14;

hence sup (f .: D) <= f . (sup D) by A3, YELLOW_0:30; :: thesis: verum

for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone holds

sup (f .: D) <= f . (sup D)

let D be non empty directed 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 up-complete & T is up-complete ) ) & 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 up-complete & T is up-complete ) ) & 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 up-complete & T is up-complete ) ) ; :: thesis: ( not f is monotone or sup (f .: D) <= f . (sup D) )

assume A2: f is monotone ; :: thesis: sup (f .: D) <= f . (sup D)

then reconsider fD = f .: D as non empty directed Subset of T by YELLOW_2:15;

A3: ex_sup_of fD,T by A1, WAYBEL_0:75;

ex_sup_of D,S by A1, WAYBEL_0:75;

then D is_<=_than sup D by YELLOW_0:30;

then f .: D is_<=_than f . (sup D) by A2, YELLOW_2:14;

hence sup (f .: D) <= f . (sup D) by A3, YELLOW_0:30; :: thesis: verum