theorem Th21: :: CLOSURE2:21

for I being set
for A, M being ManySortedSet of I
for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|