A1: f .: {} = {} by RELAT_1:149;
thus ( f is bottom-preserving implies f . (Bottom S) = Bottom T ) :: thesis: ( f . (Bottom S) = Bottom T implies f is bottom-preserving )

proof

assume f preserves_sup_of {} S ; :: according to WAYBEL34:def 16 :: thesis: f . (Bottom S) = Bottom T
then ( ex_sup_of {} S,S implies sup (f .: ({} S)) = f . (sup ({} S)) ) by WAYBEL_0:def 31;
hence f . (Bottom S) = Bottom T by RELAT_1:149, YELLOW_0:42; :: thesis: verum

end;

assume that
A2: f . (Bottom S) = Bottom T and
ex_sup_of {} S,S ; :: according to WAYBEL_0:def 31,WAYBEL34:def 16 :: thesis: ( ex_sup_of f .: ({} S),T & "\/" (f .: ({} S)),T = f . ("\/" ({} S),S) )
thus ex_sup_of f .: ({} S),T by A1, YELLOW_0:42; :: thesis: "\/" (f .: ({} S)),T = f . ("\/" ({} S),S)
thus "\/" (f .: ({} S)),T = f . ("\/" ({} S),S) by A2, RELAT_1:149; :: thesis: verum