theorem :: GROUP_1A:113

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