let G1 be addVertices of G,V; :: thesis: G1 is vertex-finite
the_Vertices_of G1 = (the_Vertices_of G) \/ V by GLIB_006:def 10;
hence G1 is vertex-finite ; :: thesis: verum