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