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 non-multi by A1, GLIB_010:89; :: thesis: verum