theorem Th7: :: YELLOW18:7

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
<^a,b^> = <^b9,a9^> by ALTCAT_2:6;