for G being Group
for H being Subgroup of G
for h being Element of G st h in H holds
H * h c= the carrier of H