theorem Th85: :: GLIB_015:85

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