theorem Th16: :: GLIB_015:16

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 ex F being PGraphMapping of G, replaceVerticesEdges (V,E) st
( F _V = V & F _E = E & F is Disomorphism )