for C1, C2 being non empty transitive AltCatStr holds
( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & ( for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) ) ) ) )