let A, B be non empty AltCatStr ; :: thesis: ( A,B are_opposite implies for a being object of holds a is object of )
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 ex a', b', c' being object of 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 holds a is object of )
hence ( not the Arrows of B = ~ the Arrows of A or ex a, b, c being object of ex a', b', c' being object of 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 holds a is object of ) ; :: thesis: verum