:: deftheorem Def17 defines bottom-preserving WAYBEL34:def 17 :
for S, T being non empty antisymmetric lower-bounded RelStr
for f being Function of S,T holds
( f is bottom-preserving iff f . (Bottom S) = Bottom T );