let G1 be addLoops of G,V; :: thesis: G1 is loopfull
the_Vertices_of G1 = the_Vertices_of G by Th15;
hence G1 is loopfull by Th5; :: thesis: verum