:: deftheorem defines antitone WAYBEL_0:def 10 :
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is antitone iff netmap (N,L) is antitone );