:: deftheorem Def18 defines ManySortedSubset PBOOLE:def 18 :
for I being set
for M, b₃ being ManySortedSet of I holds
( b₃ is ManySortedSubset of M iff b₃ c= M );