C,C opp are_opposite by Def4;
hence C opp is with_units by Th13; :: thesis: verum