theorem Th13: :: YELLOW18:13

for C, C1, C2 being non empty AltCatStr st C,C1 are_opposite holds
( C,C2 are_opposite iff 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 #) )