let G be _Graph; for v, e being object
for w being Vertex of G
for H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not v in the_Vertices_of G holds
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
let v, e be object ; for w being Vertex of G
for H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not v in the_Vertices_of G holds
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
let w be Vertex of G; for H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not v in the_Vertices_of G holds
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
let H be addAdjVertex of G,v,e,w; ( not e in the_Edges_of G & not v in the_Vertices_of G implies VertexDomRel H = (VertexDomRel G) \/ {[v,w]} )
assume A1:
( not e in the_Edges_of G & not v in the_Vertices_of G )
; VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
then consider G9 being addVertex of G,v such that
A2:
H is addEdge of G9,v,e,w
by GLIB_006:126;
A3:
not e in the_Edges_of G9
by A1, GLIB_006:def 10;
( v is Vertex of G9 & w is Vertex of G9 )
by GLIB_006:68, GLIB_006:94;
hence VertexDomRel H =
(VertexDomRel G9) \/ {[v,w]}
by A2, A3, Th27
.=
(VertexDomRel G) \/ {[v,w]}
by Th25
;
verum