:: deftheorem Def10 defines reflexive CLOSURE2:def 10 :
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is reflexive iff for x being Element of Bool M holds x c=' IT . x );