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 c -vertex by A1, GLIB_013:22; :: thesis: verum