let F be 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 DJoins v9,w9,(canGFDistinction (F,z)) . x9 holds
ex v, e, w being object st
( e DJoins 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] )
let x, z be 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 DJoins v9,w9,(canGFDistinction (F,z)) . x9 holds
ex v, e, w being object st
( e DJoins 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] )
let x9 be Element of dom (canGFDistinction (F,z)); for v9, e9, w9 being object st x <> z & x = x9 & e9 DJoins v9,w9,(canGFDistinction (F,z)) . x9 holds
ex v, e, w being object st
( e DJoins 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] )
let v9, e9, w9 be object ; ( x <> z & x = x9 & e9 DJoins v9,w9,(canGFDistinction (F,z)) . x9 implies ex v, e, w being object st
( e DJoins 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] ) )
assume A1:
( x <> z & x = x9 & e9 DJoins v9,w9,(canGFDistinction (F,z)) . x9 )
; ex v, e, w being object st
( e DJoins 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] )
reconsider x8 = x9 as Element of dom (canGFDistinction F) by FUNCT_7:30;
(canGFDistinction (F,z)) . x9 = (canGFDistinction F) . x8
by A1, FUNCT_7:32;
hence
ex v, e, w being object st
( e DJoins 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] )
by A1, Th92; verum