:: deftheorem defines antitone WAYBEL_9:def 1 :
for S, T being non empty RelStr
for f being Function of S,T holds
( f is antitone iff for x, y being Element of S st x <= y holds
f . x >= f . y );