let G be _Graph; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ;
:: thesis: verum