theorem Th38: :: MSSUBFAM:38

for I being set
for A, M being ManySortedSet of I st A c= M holds
{A} is MSSubsetFamily of M