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 chordal by A1, GLIB_010:140; :: thesis: verum