:: deftheorem defines antitone WAYBEL_0:def 5 :
for L1, L2 being RelStr
for f being Function of L1,L2 holds
( f is antitone 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 );