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 v9, e9, w9 being object st x = x9 & e9 Joins v9,w9,(canGFDistinction F) . 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 be Element of dom F; :: thesis: for x9 being Element of dom (canGFDistinction F)
for v9, e9, w9 being object st x = x9 & e9 Joins v9,w9,(canGFDistinction F) . 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); :: thesis: for v9, e9, w9 being object st x = x9 & e9 Joins v9,w9,(canGFDistinction F) . 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 = x9 & e9 Joins v9,w9,(canGFDistinction F) . 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 = x9 & e9 Joins v9,w9,(canGFDistinction F) . 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] )

per cases then ( e9 DJoins v9,w9,(canGFDistinction F) . x9 or e9 DJoins w9,v9,(canGFDistinction F) . x9 ) by GLIB_000:16;

suppose e9 DJoins v9,w9,(canGFDistinction F) . 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] )

then consider v, e, w being object such that
A2: ( 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;
take v ; :: thesis: ex 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] )
take e ; :: thesis: ex 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] )
take w ; :: thesis: ( 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] )
thus ( 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 A2, GLIB_000:16; :: thesis: verum

end;

suppose e9 DJoins w9,v9,(canGFDistinction F) . 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] )

then consider w, e, v being object such that
A3: ( e DJoins w,v,F . x & e9 = [(the_Edges_of F),x,e] & w9 = [(the_Vertices_of F),x,w] & v9 = [(the_Vertices_of F),x,v] ) by A1, Th92;
take v ; :: thesis: ex 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] )
take e ; :: thesis: ex 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] )
take w ; :: thesis: ( 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] )
thus ( 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 A3, GLIB_000:16; :: thesis: verum

end;

end;