add_inverse G is_an_inverseOp_wrt the addF of G by Th22;
hence the addF of G is having_an_inverseOp ; :: thesis: verum