for G being Group
for a being Element of G
for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")