let F be non empty Graph-yielding Function; 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; 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); 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 ; ( 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 )
; 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
;
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
;
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
;
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
;
( 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;
verum end; suppose
e9 DJoins w9,
v9,
(canGFDistinction F) . x9
;
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
;
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
;
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
;
( 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;
verum end; end;