theorem Th7: :: CLOSURE2:7

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