:: deftheorem Def2 defines antitone WAYBEL21:def 2 :
for T being non empty RelStr
for N being non empty NetStr over T holds
( N is antitone iff for i, j being Element of N st i <= j holds
N . i >= N . j );