let G be _Graph; :: thesis:
let v, e, w be object ; :: thesis:
let H be addEdge of G,v,e,w; :: thesis:
given e0 being object such that A1: e0 DJoins v,w,G ; :: thesis:

per cases ;

suppose A2: ( v in the_Vertices_of G & w in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis:

G is Subgraph of H by GLIB_006:57;
then A3: VertexDomRel G c= VertexDomRel H by Th15;

now :: thesis:

let x, y be object ; :: thesis:
assume [x,y] in VertexDomRel H ; :: thesis:
then consider e9 being object such that
A4: e9 DJoins x,y,H by Th1;

per cases by A4, GLIB_006:71;

suppose e9 DJoins x,y,G ; :: thesis:

hence [x,y] in VertexDomRel G by Th1; :: thesis:

end;

suppose A5: not e9 in the_Edges_of G ; :: thesis:

A6: the_Edges_of H = (the_Edges_of G) \/ {e} by A2, GLIB_006:def 11;
e9 in the_Edges_of H by A4, GLIB_000:def 14;
then e9 in {e} by A5, A6, XBOOLE_0:def 3;
then A7: e DJoins x,y,H by A4, TARSKI:def 1;
e DJoins v,w,H by A2, GLIB_006:105;
then ( v = x & w = y ) by A7, GLIB_009:6;
hence [x,y] in VertexDomRel G by A1, Th1; :: thesis:

end;

end;

end;

then VertexDomRel H c= VertexDomRel G by RELAT_1:def 3;
hence VertexDomRel H = VertexDomRel G by A3, XBOOLE_0:def 10; :: thesis:

end;

suppose ( not v in the_Vertices_of G or not w in the_Vertices_of G or e in the_Edges_of G ) ; :: thesis:

then G == H by GLIB_006:def 11;
hence VertexDomRel H = VertexDomRel G by Th19; :: thesis:

end;

end;