let G1 be addVertices of G,V; :: thesis: G1 is _finite
( the_Vertices_of G1 = (the_Vertices_of G) \/ V & the_Edges_of G1 = the_Edges_of G ) by Def10;
hence G1 is _finite by GLIB_000:def 17; :: thesis: verum