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