theorem :: AOFA_A00:7

for I being non empty set
for i being Element of I
for A being ManySortedSet of I
for x being set st x in A . i holds
i -singleton x is ManySortedSubset of A