theorem :: YELLOW18:8

for A, B being non empty AltCatStr st A,B are_opposite holds
for a, b being Object of A
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b holds f is Morphism of b9,a9 by Th7;