C,C opp are_opposite by Def4;
hence C opp is associative by Th12; :: thesis: verum