let G be strict Group; :: thesis: G in Subgroups G
G is Subgroup of G by GROUP_2:54;
hence G in Subgroups G by Def1; :: thesis: verum