theorem Th13: :: CLOSURE2:13

for I being set
for M being ManySortedSet of I
for SF being non empty SubsetFamily of M holds dom |.SF.| = I