let G be _Graph; :: thesis: for v being Vertex of G
for e, w being object
for H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not w in the_Vertices_of G holds
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
let v be Vertex of G; :: thesis: for e, w being object
for H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not w in the_Vertices_of G holds
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
let e, w be object ; :: thesis: for H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not w 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 w in the_Vertices_of G implies VertexDomRel H = (VertexDomRel G) \/ {[v,w]} )
assume A1: ( not e in the_Edges_of G & not w in the_Vertices_of G ) ; :: thesis: VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
then consider G9 being addVertex of G,w such that
A2: H is addEdge of G9,v,e,w by GLIB_006:125;
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