let F be non empty Graph-yielding Function; :: thesis: 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] )
let x, z be Element of dom F; :: thesis: 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] )
let x9 be Element of dom (canGFDistinction (F,z)); :: thesis: 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] )
let v9, e9, w9 be object ; :: thesis: ( x <> z & x = x9 & e9 Joins v9,w9,(canGFDistinction (F,z)) . x9 implies 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] ) )
assume A1: ( x <> z & x = x9 & e9 Joins v9,w9,(canGFDistinction (F,z)) . x9 ) ; :: thesis: 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] )
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 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] ) by A1, Th93; :: thesis: verum