let h be Element of INT.Group; :: thesis: h " = - h
reconsider g = - h as Element of INT.Group ;
h * g = 1_ INT.Group by Th35;
hence h " = - h by GROUP_1:12; :: thesis: verum