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