:: deftheorem MonDef defines monotonic FUZNORM1:def 1 :
for A being real-membered set
for f being BinOp of A holds
( f is monotonic iff for a, b, c, d being Element of A st a <= c & b <= d holds
f . (a,b) <= f . (c,d) );