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₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ ) )
A2: ( ex_sup_of {x},S & ex_sup_of {y},S ) by YELLOW_0:38;
then ( f preserves_sup_of downarrow x & f preserves_sup_of downarrow y & ex_sup_of downarrow x,S & ex_sup_of downarrow y,S ) by A1, Th32;
then A3: ( ex_sup_of f .: (downarrow x),T & ex_sup_of f .: (downarrow y),T & sup (f .: (downarrow x)) = f . (sup (downarrow x)) & sup (f .: (downarrow y)) = f . (sup (downarrow y)) ) by Def31;
assume x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ )
then A4: downarrow x c= downarrow y by Th21;
( sup (f .: (downarrow x)) = f . (sup {x}) & sup (f .: (downarrow y)) = f . (sup {y}) ) by A2, A3, Th33;
then ( sup (f .: (downarrow x)) = f . x & sup (f .: (downarrow y)) = f . y ) by YELLOW_0:39;
hence for b₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ ) by A3, A4, RELAT_1:156, YELLOW_0:34; :: thesis: verum