theorem :: GROUP_2:67

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