let G be _Graph; :: thesis: for v, e, w being object
for H being addEdge of G,v,e,w st ex e0 being object st e0 DJoins v,w,G holds
VertexDomRel H = VertexDomRel G
let v, e, w be object ; :: thesis: for H being addEdge of G,v,e,w st ex e0 being object st e0 DJoins v,w,G holds
VertexDomRel H = VertexDomRel G
let H be addEdge of G,v,e,w; :: thesis: ( ex e0 being object st e0 DJoins v,w,G implies VertexDomRel H = VertexDomRel G )
given e0 being object such that A1: e0 DJoins v,w,G ; :: thesis: VertexDomRel H = VertexDomRel G

per cases ( ( v in the_Vertices_of G & w in the_Vertices_of G & not e in the_Edges_of G ) or not v in the_Vertices_of G or not w in the_Vertices_of G or e in the_Edges_of G ) ;

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

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

now :: thesis: for x, y being object st [x,y] in VertexDomRel H holds
[x,y] in VertexDomRel G

let x, y be object ; :: thesis: ( [x,y] in VertexDomRel H implies [b₁,b₂] in VertexDomRel G )
assume [x,y] in VertexDomRel H ; :: thesis: [b₁,b₂] in VertexDomRel G
then consider e9 being object such that
A4: e9 DJoins x,y,H by Th1;

per cases ( e9 DJoins x,y,G or not e9 in the_Edges_of G ) by A4, GLIB_006:71;

suppose e9 DJoins x,y,G ; :: thesis: [b₁,b₂] in VertexDomRel G

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

end;

suppose A5: not e9 in the_Edges_of G ; :: thesis: [b₁,b₂] in VertexDomRel G

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_000:125;
hence [x,y] in VertexDomRel G by A1, Th1; :: thesis: verum

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: verum

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: VertexDomRel H = VertexDomRel G

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

end;

end;