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)) ) ;
hence f . (Bottom S) = Bottom T by YELLOW_0:42; :: thesis: verum
end;
assume that
A1: 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 YELLOW_0:42; :: thesis: "\/" ((f .: ({} S)),T) = f . ("\/" (({} S),S))
thus "\/" ((f .: ({} S)),T) = f . ("\/" (({} S),S)) by A1; :: thesis: verum