let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1 be addAdjVertexToAll of G2,v,V; :: thesis:
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
not e DJoins v,v,G1 by A1, Th38;
hence not e Joins v,v,G1 by GLIB_000:16; :: thesis:
let v1 be object ; :: thesis:
thus ( not v1 in V implies not e Joins v1,v,G1 ) :: thesis:

assume A2: not v1 in V ; :: thesis:
assume e Joins v1,v,G1 ; :: thesis:
then ( e DJoins v1,v,G1 or e DJoins v,v1,G1 ) by GLIB_000:16;
hence contradiction by A1, A2, Th38; :: thesis:

end;

let v2 be object ; :: thesis:
assume A3: ( v1 <> v & v2 <> v & e DJoins v1,v2,G1 ) ; :: thesis:
thus e DJoins v1,v2,G2 by A1, A3, Th40; :: thesis:

end;

set E = V --> (the_Edges_of G2);
take V --> (the_Edges_of G2) ; :: thesis:
thus card V = card (V --> (the_Edges_of G2)) by Lm8; :: thesis:
(the_Edges_of G2) /\ (V --> (the_Edges_of G2)) = {} by Lm6;
hence V --> (the_Edges_of G2) misses the_Edges_of G2 by XBOOLE_0:def 7; :: thesis:
thus the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2)) by A1, Def2; :: thesis:
let v1 be object ; :: thesis:
assume A4: v1 in V ; :: thesis:
set e1 = [v1,(the_Edges_of G2)];
take [v1,(the_Edges_of G2)] ; :: thesis:
the_Edges_of G2 in {(the_Edges_of G2)} by TARSKI:def 1;
then [v1,(the_Edges_of G2)] in [:V,{(the_Edges_of G2)}:] by A4, ZFMISC_1:def 2;
hence [v1,(the_Edges_of G2)] in V --> (the_Edges_of G2) by FUNCOP_1:def 2; :: thesis:
A5: [v1,(the_Edges_of G2)] DJoins v,v1,G1 by A1, A4, Th42;
hence [v1,(the_Edges_of G2)] Joins v1,v,G1 by GLIB_000:16; :: thesis:
let e2 be object ; :: thesis:
assume A6: e2 Joins v1,v,G1 ; :: thesis:
not e2 DJoins v1,v,G1 by A1, Th38;
then e2 DJoins v,v1,G1 by A6, GLIB_000:16;
hence [v1,(the_Edges_of G2)] = e2 by A1, A5, Th38; :: thesis: