theorem Th7: :: ALTCAT_2:7

for I, J being set
for A being ManySortedSet of I
for B being ManySortedSet of J st A cc= B & B cc= A holds
A = B