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 v, e, w being object st x <> z & x = x9 & e DJoins v,w,F . x holds
[(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction (F,z)) . x9
let x, z be Element of dom F; :: thesis: for x9 being Element of dom (canGFDistinction (F,z))
for v, e, w being object st x <> z & x = x9 & e DJoins v,w,F . x holds
[(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction (F,z)) . x9
let x9 be Element of dom (canGFDistinction (F,z)); :: thesis: for v, e, w being object st x <> z & x = x9 & e DJoins v,w,F . x holds
[(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction (F,z)) . x9
let v, e, w be object ; :: thesis: ( x <> z & x = x9 & e DJoins v,w,F . x implies [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction (F,z)) . x9 )
assume A1: ( x <> z & x = x9 ) ; :: thesis: ( not e DJoins v,w,F . x or [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction (F,z)) . x9 )
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 ( not e DJoins v,w,F . x or [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction (F,z)) . x9 ) by A1, Th90; :: thesis: verum