let G1 be addVertices of G,V; :: thesis: G1 is c -edge
the_Edges_of G = the_Edges_of G1 by GLIB_006:def 10;
hence G1 is c -edge by Th19; :: thesis: verum