let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let G1 be addVertex of G2,v; :: thesis:

per cases ;

suppose A1: not v in the_Vertices_of G2 ; :: thesis:

A2: {} c= the_Vertices_of G2 by XBOOLE_1:2;

now :: thesis:

thus the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by GLIB_006:def 10; :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
not e Joins v,v,G2 by A1, GLIB_000:13;
hence not e Joins v,v,G1 by GLIB_006:87; :: thesis:
let v1 be object ; :: thesis:

hereby :: thesis:

assume not v1 in {} ; :: thesis:
not e Joins v1,v,G2 by A1, GLIB_000:13;
hence not e Joins v1,v,G1 by GLIB_006:87; :: thesis:

end;

let v2 be object ; :: thesis:
assume ( v1 <> v & v2 <> v & e DJoins v1,v2,G1 ) ; :: thesis:
hence e DJoins v1,v2,G2 by GLIB_006:85; :: thesis:

end;

take E = {} ; :: thesis:
thus card {} = card E ; :: thesis:
thus E misses the_Edges_of G2 by XBOOLE_1:65; :: thesis:
thus the_Edges_of G1 = (the_Edges_of G2) \/ E by GLIB_006:def 10; :: thesis:
let v1 be object ; :: thesis:
assume v1 in {} ; :: thesis:
hence 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 ) ) ; :: thesis:

end;

hence G1 is addAdjVertexAll of G2,v, {} by A1, A2, GLIB_007:def 4; :: thesis:

end;

suppose A3: v in the_Vertices_of G2 ; :: thesis:

then G1 == G2 by ZFMISC_1:31, GLIB_006:78;
hence G1 is addAdjVertexAll of G2,v, {} by A3, GLIB_007:def 4; :: thesis:

end;

end;