theorem :: GROUP_1A:112

for G being strict addGroup
for H being Subgroup of G holds H is Subgroup of (Omega). G ;