set x = the strict Subgroup of G;
the strict Subgroup of G in Subgroups G by Def1;
hence not Subgroups G is empty ; :: thesis: verum