theorem :: GLIB_015:109

for F being non empty Graph-yielding Function
for z being Element of dom F
for z9 being Element of dom (canGFDistinction (F,z))
for v, e, w being object st z = z9 holds
( e Joins v,w,F . z iff e Joins v,w,(canGFDistinction (F,z)) . z9 )