:: deftheorem defines idempotent CLOSURE1:def 3 :
for I being set
for M being ManySortedSet of I
for IT being MSSetOp of M holds
( IT is idempotent iff for X being Element of bool M holds IT .. X = IT .. (IT .. X) );