let G be _Graph; :: thesis: for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V
for v1, e1, v2 being object st e1 Joins v1,v2,G1 holds
ex e2 being object st e2 Joins v1,v2,G2
let v be object ; :: thesis: for V being set
for G1, G2 being addAdjVertexAll of G,v,V
for v1, e1, v2 being object st e1 Joins v1,v2,G1 holds
ex e2 being object st e2 Joins v1,v2,G2
let V be set ; :: thesis: for G1, G2 being addAdjVertexAll of G,v,V
for v1, e1, v2 being object st e1 Joins v1,v2,G1 holds
ex e2 being object st e2 Joins v1,v2,G2
let G1, G2 be addAdjVertexAll of G,v,V; :: thesis: for v1, e1, v2 being object st e1 Joins v1,v2,G1 holds
ex e2 being object st e2 Joins v1,v2,G2
let v1, e1, v2 be object ; :: thesis: ( e1 Joins v1,v2,G1 implies ex e2 being object st e2 Joins v1,v2,G2 )
assume A1: e1 Joins v1,v2,G1 ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;

suppose A2: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

then consider E2 being set such that
( card V = card E2 & E2 misses the_Edges_of G & the_Edges_of G2 = (the_Edges_of G) \/ E2 ) and
A3: for w1 being object st w1 in V holds
ex e3 being object st
( e3 in E2 & e3 Joins w1,v,G2 & ( for e2 being object st e2 Joins w1,v,G2 holds
e3 = e2 ) ) by Def4;

per cases ( ( v1 = v & v2 = v ) or ( v1 = v & v2 <> v ) or ( v1 <> v & v2 = v ) or ( v1 <> v & v2 <> v ) ) ;

suppose ( v1 = v & v2 = v ) ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

hence ex e2 being object st e2 Joins v1,v2,G2 by A2, Def4, A1; :: thesis: verum

end;

suppose A4: ( v1 = v & v2 <> v ) ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

per cases ( not v2 in V or v2 in V ) ;

suppose not v2 in V ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

then not e1 Joins v2,v,G1 by A2, Def4;
hence ex e2 being object st e2 Joins v1,v2,G2 by A1, A4, GLIB_000:14; :: thesis: verum

end;

suppose v2 in V ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

then consider e3 being object such that
A5: ( e3 in E2 & e3 Joins v2,v,G2 ) and
for e2 being object st e2 Joins v2,v,G2 holds
e3 = e2 by A3;
take e3 ; :: thesis: e3 Joins v1,v2,G2
thus e3 Joins v1,v2,G2 by A5, A4, GLIB_000:14; :: thesis: verum

end;

end;

end;

suppose A6: ( v1 <> v & v2 = v ) ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

per cases ( not v1 in V or v1 in V ) ;

suppose not v1 in V ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

hence ex e2 being object st e2 Joins v1,v2,G2 by A1, A2, A6, Def4; :: thesis: verum

end;

suppose v1 in V ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

then consider e3 being object such that
A7: ( e3 in E2 & e3 Joins v1,v,G2 ) and
for e2 being object st e2 Joins v1,v,G2 holds
e3 = e2 by A3;
take e3 ; :: thesis: e3 Joins v1,v2,G2
thus e3 Joins v1,v2,G2 by A7, A6; :: thesis: verum

end;

end;

end;

suppose A8: ( v1 <> v & v2 <> v ) ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

A9: e1 Joins v1,v2,G

proof

( e1 DJoins v1,v2,G1 or e1 DJoins v2,v1,G1 ) by A1, GLIB_000:16;
then ( e1 DJoins v1,v2,G or e1 DJoins v2,v1,G ) by A2, A8, Def4;
hence e1 Joins v1,v2,G by GLIB_000:16; :: thesis: verum

end;

take e1 ; :: thesis: e1 Joins v1,v2,G2
reconsider w1 = v1, w2 = v2 as set by TARSKI:1;
e1 Joins w1,w2,G2 by A9, GLIB_006:70;
hence e1 Joins v1,v2,G2 ; :: thesis: verum

end;

end;

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: ex e2 being object st e2 Joins v1,v2,G2

then ( G1 == G & G2 == G ) by Def4;
then A10: G1 == G2 by GLIB_000:85;
take e1 ; :: thesis: e1 Joins v1,v2,G2
thus e1 Joins v1,v2,G2 by A1, A10, GLIB_000:88; :: thesis: verum

end;

end;