:: deftheorem defines preserves_sup_of WAYBEL_0:def 31 :
for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_sup_of X iff ( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) ) );