theorem :: MSSUBFAM:11

for I being set
for A, B being ManySortedSet of I st A in B holds
A is Element of B