theorem ThB62: :: GROUP_1A:263

for G being addGroup
for a being Element of G
for H being strict Subgroup of G holds
( (H * a) * (- a) = H & (H * (- a)) * a = H )