let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for E being set
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds
( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V
for E being set
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds
( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V
for E being set
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds
( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for E being set
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds
( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )
let E be set ; :: thesis: for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds
( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )
let v1, e, v2 be object ; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 implies ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) ) )
assume that
A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: ( the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 ) and
A3: ( e Joins v1,v2,G1 & not e in the_Edges_of G2 ) ; :: thesis: ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )
consider E2 being set such that
card V = card E2 and
A4: ( E2 misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E2 ) and
A5: for w being object st w in V holds
ex e1 being object st
( e1 in E2 & e1 Joins w,v,G1 & ( for e2 being object st e2 Joins w,v,G1 holds
e1 = e2 ) ) by A1, Def4;
A6: E = E2 by A2, A4, XBOOLE_1:71;

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: ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

hence ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) ) by A1, A3, Def4; :: thesis: verum

end;

suppose A7: ( v1 = v & v2 <> v ) ; :: thesis: ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

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

suppose A8: v2 in V ; :: thesis: ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

then consider e1 being object such that
A9: ( e1 in E2 & e1 Joins v2,v,G1 ) and
A10: for e2 being object st e2 Joins v2,v,G1 holds
e1 = e2 by A5;
thus e in E by A9, A6, A3, A7, A10, GLIB_000:14; :: thesis: ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) )
thus ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) by A7, A8; :: thesis: verum

end;

suppose not v2 in V ; :: thesis: ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

then not e Joins v2,v,G1 by A1, Def4;
hence ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) ) by A3, A7, GLIB_000:14; :: thesis: verum

end;

end;

end;

suppose A11: ( v1 <> v & v2 = v ) ; :: thesis: ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

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

suppose A12: v1 in V ; :: thesis: ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

then consider e1 being object such that
A13: ( e1 in E2 & e1 Joins v1,v,G1 ) and
A14: for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 by A5;
thus e in E by A13, A6, A3, A11, A14; :: thesis: ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) )
thus ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) by A11, A12; :: thesis: verum

end;

suppose not v1 in V ; :: thesis: ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

hence ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) ) by A3, A11, A1, Def4; :: thesis: verum

end;

end;

end;

suppose A15: ( v1 <> v & v2 <> v ) ; :: thesis: ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

( e DJoins v1,v2,G1 or e DJoins v2,v1,G1 ) by A3, GLIB_000:16;
then ( e DJoins v1,v2,G2 or e DJoins v2,v1,G2 ) by A1, A15, Def4;
hence ( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) ) by A3, GLIB_000:def 14; :: thesis: verum

end;

end;