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 DJoins v9,w9,(canGFDistinction F) . x9 holds
ex v, e, w being object st
( 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] )
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 DJoins v9,w9,(canGFDistinction F) . x9 holds
ex v, e, w being object st
( 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] )
let x9 be Element of dom (canGFDistinction F); :: thesis: for v9, e9, w9 being object st x = x9 & e9 DJoins v9,w9,(canGFDistinction F) . x9 holds
ex v, e, w being object st
( 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] )
let v9, e9, w9 be object ; :: thesis: ( x = x9 & e9 DJoins v9,w9,(canGFDistinction F) . x9 implies ex v, e, w being object st
( 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] ) )
assume A1: x = x9 ; :: thesis: ( not e9 DJoins v9,w9,(canGFDistinction F) . x9 or ex v, e, w being object st
( 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] ) )
then consider G being PGraphMapping of F . x,(canGFDistinction F) . x9 such that
A2: G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) and
A3: G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) and
A4: G is Disomorphism by Th85;
assume A5: e9 DJoins v9,w9,(canGFDistinction F) . x9 ; :: thesis: ex v, e, w being object st
( 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] )
then A6: e9 Joins v9,w9,(canGFDistinction F) . x9 by GLIB_000:16;
A7: the_Vertices_of ((canGFDistinction F) . x9) = (the_Vertices_of (canGFDistinction F)) . x by A1, Def8
.= [:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] by Th83
.= rng (renameElementsDistinctlyFunc ((the_Vertices_of F),x)) by Th80 ;
x in dom F ;
then A8: ( x in dom (the_Vertices_of F) & x in dom (the_Edges_of F) ) by Def4, Def5;
v9 in the_Vertices_of ((canGFDistinction F) . x9) by A6, GLIB_000:13;
then consider v being object such that
A9: ( v in (the_Vertices_of F) . x & v9 = [(the_Vertices_of F),x,v] ) by A7, A8, Th79;
w9 in the_Vertices_of ((canGFDistinction F) . x9) by A6, GLIB_000:13;
then consider w being object such that
A10: ( w in (the_Vertices_of F) . x & w9 = [(the_Vertices_of F),x,w] ) by A7, A8, Th79;
A11: the_Edges_of ((canGFDistinction F) . x9) = (the_Edges_of (canGFDistinction F)) . x by A1, Def9
.= [:{[(the_Edges_of F),x]},((the_Edges_of F) . x):] by Th84
.= rng (renameElementsDistinctlyFunc ((the_Edges_of F),x)) by Th80 ;
e9 in the_Edges_of ((canGFDistinction F) . x9) by A6, GLIB_000:def 13;
then consider e being object such that
A12: ( e in (the_Edges_of F) . x & e9 = [(the_Edges_of F),x,e] ) by A8, A11, Th79;
take v ; :: thesis: ex e, w being object st
( 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] )
take e ; :: thesis: ex w being object st
( 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] )
take w ; :: thesis: ( 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] )
( the_Edges_of (F . x) = (the_Edges_of F) . x & the_Vertices_of (F . x) = (the_Vertices_of F) . x ) by Def8, Def9;
then ( dom (G _E) = (the_Edges_of F) . x & dom (G _V) = (the_Vertices_of F) . x ) by A4, GLIB_010:def 11;
then A13: ( e in dom (G _E) & v in dom (G _V) & w in dom (G _V) ) by A9, A10, A12;
(G _E) . e DJoins v9,w9,(canGFDistinction F) . x9 by A3, A5, A8, A12, Th78;
then (G _E) . e DJoins (G _V) . v,w9,(canGFDistinction F) . x9 by A2, A8, A9, Th78;
then (G _E) . e DJoins (G _V) . v,(G _V) . w,(canGFDistinction F) . x9 by A2, A8, A10, Th78;
hence e DJoins v,w,F . x by A4, A13, GLIB_010:def 17; :: thesis: ( e9 = [(the_Edges_of F),x,e] & v9 = [(the_Vertices_of F),x,v] & w9 = [(the_Vertices_of F),x,w] )
thus ( e9 = [(the_Edges_of F),x,e] & v9 = [(the_Vertices_of F),x,v] & w9 = [(the_Vertices_of F),x,w] ) by A9, A10, A12; :: thesis: verum