consider F being PGraphMapping of G, replaceVerticesEdges (V,E) such that
A1: ( F _V = V & F _E = E & F is Disomorphism ) by Th16;
thus replaceVerticesEdges (V,E) is loopfull by A1, GLIB_012:10; :: thesis: verum