theorem Th8: :: ALTCAT_2:8

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