let G be _Graph; 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; 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 ; 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; ( not e in the_Edges_of G implies VertexDomRel H = (VertexDomRel G) \/ {[v,w]} )
assume A1:
not e in the_Edges_of G
; VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
now 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 ;
( ( [x,y] in VertexDomRel H implies [x,y] in (VertexDomRel G) \/ {[v,w]} ) & ( [x,y] in (VertexDomRel G) \/ {[v,w]} implies [b1,b2] in VertexDomRel H ) )hereby ( [x,y] in (VertexDomRel G) \/ {[v,w]} implies [b1,b2] in VertexDomRel H )
assume
[x,y] in VertexDomRel H
;
[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 A3:
not
e0 in the_Edges_of G
;
[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_009:6;
then
[x,y] in {[v,w]}
by TARSKI:def 1;
hence
[x,y] in (VertexDomRel G) \/ {[v,w]}
by XBOOLE_0:def 3;
verum end;
end; assume
[x,y] in (VertexDomRel G) \/ {[v,w]}
;
[b1,b2] in VertexDomRel H end;
hence
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
by RELAT_1:def 2; verum