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
VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}
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
VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}
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
VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}
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 VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]} )
assume A1: ( not e in the_Edges_of G & not v in the_Vertices_of G ) ; :: thesis: VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}
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 VertexAdjSymRel H = (VertexAdjSymRel G9) \/ {[v,w],[w,v]} by A2, A3, Th57
.= (VertexAdjSymRel G) \/ {[v,w],[w,v]} by Th55 ;
:: thesis: verum