for G being addGroup
for H being Subgroup of G st G is Abelian addGroup holds
H is Abelian