:: deftheorem Def9 defines monotone WAYBEL11:def 9 :
for R being non empty reflexive RelStr
for N being non empty NetStr over R holds
( N is monotone iff for i, j being Element of N st i <= j holds
N . i <= N . j );