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