let A, B be non empty AltCatStr ; :: thesis: ( A,B are_opposite implies for a being object of A holds a is object of B )
assume the carrier of A = the carrier of B ; :: according to YELLOW18:def 3 :: thesis: ( not the Arrows of B = ~ the Arrows of A or ex a, b, c being object of A ex a9, b9, c9 being object of B st
( a9 = a & b9 = b & c9 = c & not the Comp of B . (a9,b9,c9) = ~ ( the Comp of A . (c,b,a)) ) or for a being object of A holds a is object of B )
hence ( not the Arrows of B = ~ the Arrows of A or ex a, b, c being object of A ex a9, b9, c9 being object of B st
( a9 = a & b9 = b & c9 = c & not the Comp of B . (a9,b9,c9) = ~ ( the Comp of A . (c,b,a)) ) or for a being object of A holds a is object of B ) ; :: thesis: verum