for G being addGroup
for H being strict Subgroup of G st G is Abelian addGroup holds
H is normal by Th73;