let G be _Graph; :: thesis: for v, w being Vertex of G
for e being object
for H being addEdge of G,v,e,w st not e in the_Edges_of G holds
VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}
let v, w be Vertex of G; :: thesis: for e being object
for H being addEdge of G,v,e,w st not e in the_Edges_of G holds
VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}
let e be object ; :: thesis: for H being addEdge of G,v,e,w st not e in the_Edges_of G holds
VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}
let H be addEdge of G,v,e,w; :: thesis: ( not e in the_Edges_of G implies VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]} )
assume A1: not e in the_Edges_of G ; :: thesis: VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}
set R = VertexDomRel G;
set U = (VertexDomRel G) \/ {[v,w]};
A2: ((VertexDomRel G) \/ {[v,w]}) ~ = ((VertexDomRel G) ~) \/ ({[v,w]} ~) by RELAT_1:23;
thus VertexAdjSymRel H = ((VertexDomRel G) \/ {[v,w]}) \/ ((VertexDomRel H) ~) by A1, Th27
.= ((VertexDomRel G) \/ {[v,w]}) \/ (((VertexDomRel G) \/ {[v,w]}) ~) by A1, Th27
.= ((VertexDomRel G) \/ {[v,w]}) \/ (((VertexDomRel G) ~) \/ {[w,v]}) by A2, GLIBPRE0:12
.= (((VertexDomRel G) \/ {[v,w]}) \/ ((VertexDomRel G) ~)) \/ {[w,v]} by XBOOLE_1:4
.= (((VertexDomRel G) \/ ((VertexDomRel G) ~)) \/ {[v,w]}) \/ {[w,v]} by XBOOLE_1:4
.= ((VertexDomRel G) \/ ((VertexDomRel G) ~)) \/ ({[v,w]} \/ {[w,v]}) by XBOOLE_1:4
.= (VertexAdjSymRel G) \/ {[v,w],[w,v]} by ENUMSET1:1 ; :: thesis: verum