theorem :: GROUP_1A:95
for G being addGroup
for H being Subgroup of G holds add_inverse H = (add_inverse G) | the carrier of H