theorem Th22: :: ALTCAT_2:22

for C1, C2 being AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C1 holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)