let G1 be addVertices of G,X; :: thesis: G1 is edgeless
the_Edges_of G1 = the_Edges_of G by GLIB_006:def 10;
hence G1 is edgeless ; :: thesis: verum