let S, T be with_suprema Poset; :: thesis: for f being Function of S,T
for x, y being Element of S holds
( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) )
let f be Function of S,T; :: thesis: for x, y being Element of S holds
( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) )
let x, y be Element of S; :: thesis: ( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) )
A1: dom f = the carrier of S by FUNCT_2:def 1;

hereby :: thesis: ( f . (x "\/" y) = (f . x) "\/" (f . y) implies f preserves_sup_of {x,y} )

A2: ex_sup_of {x,y},S by YELLOW_0:20;
assume A3: f preserves_sup_of {x,y} ; :: thesis: f . (x "\/" y) = (f . x) "\/" (f . y)
thus f . (x "\/" y) = f . (sup {x,y}) by YELLOW_0:41
.= sup (f .: {x,y}) by A3, A2
.= sup {(f . x),(f . y)} by A1, FUNCT_1:60
.= (f . x) "\/" (f . y) by YELLOW_0:41 ; :: thesis: verum

end;

assume A4: f . (x "\/" y) = (f . x) "\/" (f . y) ; :: thesis: f preserves_sup_of {x,y}
assume ex_sup_of {x,y},S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: {x,y},T & "\/" ((f .: {x,y}),T) = f . ("\/" ({x,y},S)) )
f .: {x,y} = {(f . x),(f . y)} by A1, FUNCT_1:60;
hence ex_sup_of f .: {x,y},T by YELLOW_0:20; :: thesis: "\/" ((f .: {x,y}),T) = f . ("\/" ({x,y},S))
thus sup (f .: {x,y}) = sup {(f . x),(f . y)} by A1, FUNCT_1:60
.= (f . x) "\/" (f . y) by YELLOW_0:41
.= f . (sup {x,y}) by A4, YELLOW_0:41 ; :: thesis: verum