let G1 be addVertices of G,V; :: thesis: not G1 is _finite
the_Vertices_of G1 = (the_Vertices_of G) \/ V by Def10;
hence not G1 is _finite ; :: thesis: verum