:: deftheorem Def12 defines idempotent CLOSURE2:def 12 :
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is idempotent iff for x being Element of Bool M holds IT . x = IT . (IT . x) );