:: deftheorem defines monotone WAYBEL_1:def 2 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is monotone iff for x, y being Element of L1 st x <= y holds
f . x <= f . y );