let F be non empty Graph-yielding Function; :: thesis: for x being Element of dom F
for x9 being Element of dom (canGFDistinction F)
for v, e, w being object st x = x9 & e Joins v,w,F . x holds
[(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9
let x be Element of dom F; :: thesis: for x9 being Element of dom (canGFDistinction F)
for v, e, w being object st x = x9 & e Joins v,w,F . x holds
[(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9
let x9 be Element of dom (canGFDistinction F); :: thesis: for v, e, w being object st x = x9 & e Joins v,w,F . x holds
[(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9
let v, e, w be object ; :: thesis: ( x = x9 & e Joins v,w,F . x implies [(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9 )
assume A1: x = x9 ; :: thesis: ( not e Joins v,w,F . x or [(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9 )
assume e Joins v,w,F . x ; :: thesis: [(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9

per cases then ( e DJoins v,w,F . x or e DJoins w,v,F . x ) by GLIB_000:16;

suppose e DJoins v,w,F . x ; :: thesis: [(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9

then [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9 by A1, Th90;
hence [(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9 by GLIB_000:16; :: thesis: verum

end;

suppose e DJoins w,v,F . x ; :: thesis: [(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9

then [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,w],[(the_Vertices_of F),x,v],(canGFDistinction F) . x9 by A1, Th90;
hence [(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9 by GLIB_000:16; :: thesis: verum

end;

end;