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