let G, G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1 be addAdjVertexAll of G,v,V; :: thesis:
assume A1: G1 == G2 ; :: thesis:

per cases ;

suppose A2: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis:

then consider E being set such that
A3: ( card V = card E & E misses the_Edges_of G ) and
A4: the_Edges_of G1 = (the_Edges_of G) \/ E and
A5: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by Def4;

A6: now :: thesis:

the_Vertices_of G1 = (the_Vertices_of G) \/ {v} by A2, Def4;
hence the_Vertices_of G2 = (the_Vertices_of G) \/ {v} by A1, GLIB_000:def 34; :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
not e Joins v,v,G1 by A2, Def4;
hence not e Joins v,v,G2 by A1, GLIB_000:88; :: thesis:
let v1 be object ; :: thesis:

hereby :: thesis:

assume not v1 in V ; :: thesis:
then not e Joins v1,v,G1 by A2, Def4;
hence not e Joins v1,v,G2 by A1, GLIB_000:88; :: thesis:

end;

let v2 be object ; :: thesis:
assume that
A7: ( v1 <> v & v2 <> v ) and
A8: e DJoins v1,v2,G2 ; :: thesis:
e DJoins v1,v2,G1 by A8, A1, GLIB_000:88;
hence e DJoins v1,v2,G by A2, A7, Def4; :: thesis:

end;

take E = E; :: thesis:
thus ( card V = card E & E misses the_Edges_of G ) by A3; :: thesis:
thus the_Edges_of G2 = (the_Edges_of G) \/ E by A4, A1, GLIB_000:def 34; :: thesis:
let v1 be object ; :: thesis:
assume v1 in V ; :: thesis:
then consider e1 being object such that
A9: ( e1 in E & e1 Joins v1,v,G1 ) and
A10: for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 by A5;
take e1 = e1; :: thesis:
thus ( e1 in E & e1 Joins v1,v,G2 ) by A1, A9, GLIB_000:88; :: thesis:
let e2 be object ; :: thesis:
assume e2 Joins v1,v,G2 ; :: thesis:
then e2 Joins v1,v,G1 by A1, GLIB_000:88;
hence e1 = e2 by A10; :: thesis:

end;

G2 is Supergraph of G1 by A1, GLIB_006:59;
then G2 is Supergraph of G by GLIB_006:62;
hence G2 is addAdjVertexAll of G,v,V by A2, A6, Def4; :: thesis:

end;

suppose A11: ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis:

then G == G1 by Def4;
then A12: G == G2 by A1, GLIB_000:85;
then G2 is Supergraph of G by GLIB_006:59;
hence G2 is addAdjVertexAll of G,v,V by A11, A12, Def4; :: thesis:

end;

end;