theorem :: GLIB_015:113

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))
for v9, e9, w9 being object st x <> z & x = x9 & e9 Joins v9,w9,(canGFDistinction (F,z)) . 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] )