for F being non empty Graph-yielding Function
for x being Element of dom F
for x9 being Element of dom (canGFDistinction F)
for v9, e9, w9 being object st x = x9 & e9 Joins v9,w9,(canGFDistinction F) . x9 holds
ex v, e, w being object st
( e Joins v,w,F . x & e9 = [(the_Edges_of F),x,e] & v9 = [(the_Vertices_of F),x,v] & w9 = [(the_Vertices_of F),x,w] )