let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e, v1, v2 being object st v1 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e, v1, v2 being object st v1 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2
let V be set ; :: thesis: for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e, v1, v2 being object st v1 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2
let G1 be addAdjVertexToAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies for e, v1, v2 being object st v1 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 )
assume ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: for e, v1, v2 being object st v1 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2
then A1: ( the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} & the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2)) & the_Source_of G1 = (the_Source_of G2) +* ((V --> (the_Edges_of G2)) --> v) ) by Def2;
let e, v1, v2 be object ; :: thesis: ( v1 <> v & e DJoins v1,v2,G1 implies e DJoins v1,v2,G2 )
assume A2: v1 <> v ; :: thesis: ( not e DJoins v1,v2,G1 or e DJoins v1,v2,G2 )
assume A3: e DJoins v1,v2,G1 ; :: thesis: e DJoins v1,v2,G2
then A4: e in the_Edges_of G1 by GLIB_000:def 14;
A5: e in the_Edges_of G2

proof

assume not e in the_Edges_of G2 ; :: thesis: contradiction
then A6: e in V --> (the_Edges_of G2) by A1, A4, XBOOLE_0:def 3;
then e in dom ((V --> (the_Edges_of G2)) --> v) ;
then (the_Source_of G1) . e = ((V --> (the_Edges_of G2)) --> v) . e by A1, FUNCT_4:13
.= v by A6, FUNCOP_1:7 ;
hence contradiction by A2, A3, GLIB_000:def 14; :: thesis: verum

end;

reconsider e1 = e as set by TARSKI:1;
( (the_Source_of G1) . e1 = (the_Source_of G2) . e1 & (the_Target_of G1) . e1 = (the_Target_of G2) . e1 ) by A5, GLIB_006:def 9;
then ( v1 = (the_Source_of G2) . e1 & v2 = (the_Target_of G2) . e1 ) by A3, GLIB_000:def 14;
hence e DJoins v1,v2,G2 by A5, GLIB_000:def 14; :: thesis: verum