:: deftheorem defines cc= ALTCAT_2:def 2 :
for I, J being set
for A being ManySortedSet of I
for B being ManySortedSet of J holds
( A cc= B iff ( I c= J & ( for i being set st i in I holds
A . i c= B . i ) ) );