for G being addGroup
for g being Element of G
for H being Subgroup of G st g in carr H holds
- g in carr H