:: deftheorem Def11 defines monotonic CLOSURE2:def 11 :
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is monotonic iff for x, y being Element of Bool M st x c=' y holds
IT . x c=' IT . y );