theorem Th7: :: TOPS_5:7

for i being object
for J being ManySortedSet of {i} holds J = {i} --> (J . i)