theorem Th13: :: AOFA_L00:13

for I being set
for X being ManySortedSet of I
for S being ManySortedSubset of X
for x being object holds S . x is Subset of (X . x)