A1: f .: {} = {} by RELAT_1:116;
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:116, 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:116; :: thesis: verum