for G being addGroup
for H being Subgroup of G holds 0_ G in H