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 a', b', c' being object of B st
( a' = a & b' = b & c' = c & not the Comp of B . a',b',c' = ~ (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 a', b', c' being object of B st
( a' = a & b' = b & c' = c & not the Comp of B . a',b',c' = ~ (the Comp of A . c,b,a) ) or for a being object of A holds a is object of B ) ; :: thesis: verum