let G be Group; :: thesis: G is Subgroup of (Omega). G
G is Subgroup of G by GROUP_2:54;
hence G is Subgroup of (Omega). G by GROUP_2:57; :: thesis: verum