:: deftheorem Def4 defines opp YELLOW18:def 4 :
for C being non empty transitive AltCatStr
for b₂ being non empty transitive strict AltCatStr holds
( b₂ = C opp iff C,b₂ are_opposite );