let G2 be _Graph; :: thesis:
let v1 be Vertex of G2; :: thesis:
let e, v2 be object ; :: thesis:
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis:
assume A1: ( not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis:
let e1, w be object ; :: thesis:
assume ( w <> v1 or e1 <> e ) ; :: thesis:

per cases ;

suppose A2: w <> v1 ; :: thesis:

assume A3: e1 Joins w,v2,G1 ; :: thesis:

per cases by Th76;

suppose e1 Joins w,v2,G2 ; :: thesis:

hence contradiction by A1, GLIB_000:13; :: thesis:

end;

suppose A4: not e1 in the_Edges_of G2 ; :: thesis:

A5: e1 in the_Edges_of G1 by A3, GLIB_000:def 13;
the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, Def12;
then e1 in {e} by A4, A5, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 Joins v1,v2,G1 by A1, Th135;

per cases by A3, GLIB_000:15;

suppose ( v1 = w & v2 = v2 ) ; :: thesis:

hence contradiction by A2; :: thesis:

end;

suppose ( v1 = v2 & v2 = w ) ; :: thesis:

hence contradiction by A1; :: thesis:

end;

end;

end;

end;

end;

suppose A6: e1 <> e ; :: thesis:

assume A7: e1 Joins w,v2,G1 ; :: thesis:

per cases by Th76;

suppose e1 Joins w,v2,G2 ; :: thesis:

hence contradiction by A1, GLIB_000:13; :: thesis:

end;

suppose A8: not e1 in the_Edges_of G2 ; :: thesis:

A9: e1 in the_Edges_of G1 by A7, GLIB_000:def 13;
the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, Def12;
then e1 in {e} by A8, A9, XBOOLE_0:def 3;
hence contradiction by A6, TARSKI:def 1; :: thesis:

end;

end;

end;

end;