let h be Element of INT.Group; :: thesis: h " = - h
- h in INT by INT_1:def 2;
then reconsider g = - h as Element of INT.Group ;
h * g = 1_ INT.Group by Th13;
hence h " = - h by GROUP_1:12; :: thesis: verum