let G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v1,v,G1
let v be object ; for V being set
for G1 being addAdjVertexFromAll of G2,v,V
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v1,v,G1
let V be set ; for G1 being addAdjVertexFromAll of G2,v,V
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v1,v,G1
let G1 be addAdjVertexFromAll of G2,v,V; for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v1,v,G1
let v1 be object ; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V implies [v1,(the_Edges_of G2)] DJoins v1,v,G1 )
assume A1:
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V )
; [v1,(the_Edges_of G2)] DJoins v1,v,G1
then A2:
( the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2)) & the_Source_of G1 = (the_Source_of G2) +* (pr1 (V,{(the_Edges_of G2)})) & the_Target_of G1 = (the_Target_of G2) +* ((V --> (the_Edges_of G2)) --> v) )
by Def3;
set e = [v1,(the_Edges_of G2)];
A3:
the_Edges_of G2 in {(the_Edges_of G2)}
by TARSKI:def 1;
then A4:
[v1,(the_Edges_of G2)] in [:V,{(the_Edges_of G2)}:]
by A1, ZFMISC_1:def 2;
then A5:
[v1,(the_Edges_of G2)] in V --> (the_Edges_of G2)
by FUNCOP_1:def 2;
then A6:
[v1,(the_Edges_of G2)] in dom ((V --> (the_Edges_of G2)) --> v)
;
A7:
[v1,(the_Edges_of G2)] in dom (pr1 (V,{(the_Edges_of G2)}))
by A4, FUNCT_3:def 4;
A8:
[v1,(the_Edges_of G2)] in the_Edges_of G1
by A2, A5, XBOOLE_0:def 3;
A9: (the_Target_of G1) . [v1,(the_Edges_of G2)] =
((V --> (the_Edges_of G2)) --> v) . [v1,(the_Edges_of G2)]
by A2, A6, FUNCT_4:13
.=
v
by A5, FUNCOP_1:7
;
(the_Source_of G1) . [v1,(the_Edges_of G2)] =
(pr1 (V,{(the_Edges_of G2)})) . [v1,(the_Edges_of G2)]
by A2, A7, FUNCT_4:13
.=
(pr1 (V,{(the_Edges_of G2)})) . (v1,(the_Edges_of G2))
by BINOP_1:def 1
.=
v1
by A1, A3, FUNCT_3:def 4
;
hence
[v1,(the_Edges_of G2)] DJoins v1,v,G1
by A8, A9, GLIB_000:def 14; verum