let G be _Graph; :: thesis: for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G holds replaceVerticesEdges (V,E) is G -Disomorphic
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; :: thesis: for E being one-to-one ManySortedSet of the_Edges_of G holds replaceVerticesEdges (V,E) is G -Disomorphic
let E be one-to-one ManySortedSet of the_Edges_of G; :: thesis: replaceVerticesEdges (V,E) is G -Disomorphic
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 G -Disomorphic by A1, GLIB_010:def 24; :: thesis: verum