:: deftheorem defines are_opposite YELLOW18:def 3 :
for C1, C2 being non empty AltCatStr holds
( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) ) );