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