theorem Th9:
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 ) ) ) ) )