let G be strict addGroup; :: thesis: G in Subgroups G
G is Subgroup of G by ThA54;
hence G in Subgroups G by Def1; :: thesis: verum