let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2
let v1, e, v2 be object ; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 implies e Joins v1,v2,G2 )
assume that
A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: ( v1 <> v & v2 <> v ) and
A3: e Joins v1,v2,G1 ; :: thesis: e Joins v1,v2,G2

per cases ( e DJoins v1,v2,G1 or e DJoins v2,v1,G1 ) by A3, GLIB_000:16;

suppose e DJoins v1,v2,G1 ; :: thesis: e Joins v1,v2,G2

then e DJoins v1,v2,G2 by A1, A2, Def4;
hence e Joins v1,v2,G2 by GLIB_000:16; :: thesis: verum

end;

suppose e DJoins v2,v1,G1 ; :: thesis: e Joins v1,v2,G2

then e DJoins v2,v1,G2 by A1, A2, Def4;
hence e Joins v1,v2,G2 by GLIB_000:16; :: thesis: verum

end;

end;