theorem Th103: :: GLIB_015:103

for F being non empty Graph-yielding Function
for x, z being Element of dom F
for x9 being Element of dom (canGFDistinction (F,z)) st x <> z & x = x9 holds
ex G being PGraphMapping of F . x,(canGFDistinction (F,z)) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism )