let G1 be addLoops of G,V; :: thesis: G1 is vertex-finite
the_Vertices_of G1 = the_Vertices_of G by GLIB_012:15;
hence G1 is vertex-finite ; :: thesis: verum