:: deftheorem defines monotone ORDERS_3:def 5 :
for L1, L2 being RelStr
for f being Function of L1,L2 holds
( f is monotone iff for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a <= b );