let G be _Graph; :: thesis: for v, w being Vertex of G
for e being object
for H being addEdge of G,v,e,w st not e in the_Edges_of G holds
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
let v, w be Vertex of G; :: thesis: for e being object
for H being addEdge of G,v,e,w st not e in the_Edges_of G holds
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
let e be object ; :: thesis: for H being addEdge of G,v,e,w st not e in the_Edges_of G holds
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
let H be addEdge of G,v,e,w; :: thesis: ( not e in the_Edges_of G implies VertexDomRel H = (VertexDomRel G) \/ {[v,w]} )
assume A1: not e in the_Edges_of G ; :: thesis: VertexDomRel H = (VertexDomRel G) \/ {[v,w]}

now :: thesis: for x, y being object holds
( ( [x,y] in VertexDomRel H implies [x,y] in (VertexDomRel G) \/ {[v,w]} ) & ( [x,y] in (VertexDomRel G) \/ {[v,w]} implies [x,y] in VertexDomRel H ) )

let x, y be object ; :: thesis: ( ( [x,y] in VertexDomRel H implies [x,y] in (VertexDomRel G) \/ {[v,w]} ) & ( [x,y] in (VertexDomRel G) \/ {[v,w]} implies [b₁,b₂] in VertexDomRel H ) )

hereby :: thesis: ( [x,y] in (VertexDomRel G) \/ {[v,w]} implies [b₁,b₂] in VertexDomRel H )

assume [x,y] in VertexDomRel H ; :: thesis: [x,y] in (VertexDomRel G) \/ {[v,w]}
then consider e0 being object such that
A2: e0 DJoins x,y,H by Th1;

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

suppose e0 DJoins x,y,G ; :: thesis: [x,y] in (VertexDomRel G) \/ {[v,w]}

then [x,y] in VertexDomRel G by Th1;
hence [x,y] in (VertexDomRel G) \/ {[v,w]} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A3: not e0 in the_Edges_of G ; :: thesis: [x,y] in (VertexDomRel G) \/ {[v,w]}

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

end;

end;

end;

assume [x,y] in (VertexDomRel G) \/ {[v,w]} ; :: thesis: [b₁,b₂] in VertexDomRel H

per cases then ( [x,y] in VertexDomRel G or [x,y] in {[v,w]} ) by XBOOLE_0:def 3;

suppose A6: [x,y] in VertexDomRel G ; :: thesis: [b₁,b₂] in VertexDomRel H

G is Subgraph of H by GLIB_006:57;
hence [x,y] in VertexDomRel H by A6, Th15, TARSKI:def 3; :: thesis: verum

end;

suppose [x,y] in {[v,w]} ; :: thesis: [b₁,b₂] in VertexDomRel H

then [x,y] = [v,w] by TARSKI:def 1;
hence [x,y] in VertexDomRel H by A1, Th1, GLIB_006:105; :: thesis: verum

end;

end;

end;

hence VertexDomRel H = (VertexDomRel G) \/ {[v,w]} by RELAT_1:def 2; :: thesis: verum