:: deftheorem defines waybelow-preserving WAYBEL34:def 8 :
for S, T being non empty reflexive RelStr
for f being Function of S,T holds
( f is waybelow-preserving iff for x, y being Element of S st x << y holds
f . x << f . y );