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