:: deftheorem defines monotonic CLOSURE1:def 2 :
for I being set
for M being ManySortedSet of I
for IT being MSSetOp 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 );