theorem :: ALTCAT_2:9

for I being set
for A, B being ManySortedSet of I holds
( A cc= B iff A c= B ) ;