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 monotone

let f be Function of S,T; :: thesis: ( ( for X being Ideal of S holds f preserves_sup_of X ) implies f is monotone )

assume A1: for X being Ideal of S holds f preserves_sup_of X ; :: thesis: f is monotone

let x, y be Element of S; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b_{1}, b_{2} being Element of the carrier of T holds

( not b_{1} = f . x or not b_{2} = f . y or b_{1} <= b_{2} ) )

A2: ex_sup_of {x},S by YELLOW_0:38;

A3: ex_sup_of {y},S by YELLOW_0:38;

A4: f preserves_sup_of downarrow x by A1;

A5: f preserves_sup_of downarrow y by A1;

A6: ex_sup_of downarrow x,S by A2, Th32;

A7: ex_sup_of downarrow y,S by A3, Th32;

A8: ex_sup_of f .: (downarrow x),T by A4, A6;

A9: ex_sup_of f .: (downarrow y),T by A5, A7;

A10: sup (f .: (downarrow x)) = f . (sup (downarrow x)) by A4, A6;

A11: sup (f .: (downarrow y)) = f . (sup (downarrow y)) by A5, A7;

assume x <= y ; :: thesis: for b_{1}, b_{2} being Element of the carrier of T holds

( not b_{1} = f . x or not b_{2} = f . y or b_{1} <= b_{2} )

then A12: downarrow x c= downarrow y by Th21;

A13: sup (f .: (downarrow x)) = f . (sup {x}) by A10, Th33, YELLOW_0:38;

A14: sup (f .: (downarrow y)) = f . (sup {y}) by A11, Th33, YELLOW_0:38;

A15: sup (f .: (downarrow x)) = f . x by A13, YELLOW_0:39;

sup (f .: (downarrow y)) = f . y by A14, YELLOW_0:39;

hence for b_{1}, b_{2} being Element of the carrier of T holds

( not b_{1} = f . x or not b_{2} = f . y or b_{1} <= b_{2} )
by A8, A9, A12, A15, RELAT_1:123, YELLOW_0:34; :: thesis: verum

f is monotone

let f be Function of S,T; :: thesis: ( ( for X being Ideal of S holds f preserves_sup_of X ) implies f is monotone )

assume A1: for X being Ideal of S holds f preserves_sup_of X ; :: thesis: f is monotone

let x, y be Element of S; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b

( not b

A2: ex_sup_of {x},S by YELLOW_0:38;

A3: ex_sup_of {y},S by YELLOW_0:38;

A4: f preserves_sup_of downarrow x by A1;

A5: f preserves_sup_of downarrow y by A1;

A6: ex_sup_of downarrow x,S by A2, Th32;

A7: ex_sup_of downarrow y,S by A3, Th32;

A8: ex_sup_of f .: (downarrow x),T by A4, A6;

A9: ex_sup_of f .: (downarrow y),T by A5, A7;

A10: sup (f .: (downarrow x)) = f . (sup (downarrow x)) by A4, A6;

A11: sup (f .: (downarrow y)) = f . (sup (downarrow y)) by A5, A7;

assume x <= y ; :: thesis: for b

( not b

then A12: downarrow x c= downarrow y by Th21;

A13: sup (f .: (downarrow x)) = f . (sup {x}) by A10, Th33, YELLOW_0:38;

A14: sup (f .: (downarrow y)) = f . (sup {y}) by A11, Th33, YELLOW_0:38;

A15: sup (f .: (downarrow x)) = f . x by A13, YELLOW_0:39;

sup (f .: (downarrow y)) = f . y by A14, YELLOW_0:39;

hence for b

( not b