theorem Th3: :: PBOOLE:3

for I being set
for X, Y being ManySortedSet of I st ( for i being object st i in I holds
X . i = Y . i ) holds
X = Y