theorem Th17: :: GLIB_015:17

for G being _Graph
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