:: deftheorem Def1 defines Bool CLOSURE2:def 1 :
for I being set
for M being ManySortedSet of I
for b₃ being set holds
( b₃ = Bool M iff for x being object holds
( x in b₃ iff x is ManySortedSubset of M ) );