rng S = the_Vertices_of G by Def12;
hence x .. S is non zero Element of NAT by FINSEQ_4:31; :: thesis: verum