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 v,w are_adjacent holds
VertexAdjSymRel H = VertexAdjSymRel G
let v, w be Vertex of G; :: thesis: for e being object
for H being addEdge of G,v,e,w st v,w are_adjacent holds
VertexAdjSymRel H = VertexAdjSymRel G
let e be object ; :: thesis: for H being addEdge of G,v,e,w st v,w are_adjacent holds
VertexAdjSymRel H = VertexAdjSymRel G
let H be addEdge of G,v,e,w; :: thesis: ( v,w are_adjacent implies VertexAdjSymRel H = VertexAdjSymRel G )
assume v,w are_adjacent ; :: thesis: VertexAdjSymRel H = VertexAdjSymRel G
then consider e0 being object such that
A1: e0 Joins v,w,G by CHORD:def 3;
per cases ( not e in the_Edges_of G or e in the_Edges_of G ) ;
suppose A2: not e in the_Edges_of G ; :: thesis: VertexAdjSymRel H = VertexAdjSymRel G
per cases ( e0 DJoins v,w,G or e0 DJoins w,v,G ) by A1, GLIB_000:16;
suppose e0 DJoins w,v,G ; :: thesis: VertexAdjSymRel H = VertexAdjSymRel G
then A4: [w,v] in VertexDomRel G by Th1;
then A5: [v,w] in (VertexDomRel G) ~ by RELAT_1:def 7;
set R = VertexDomRel G;
set U = (VertexDomRel G) \/ {[v,w]};
A6: ((VertexDomRel G) \/ {[v,w]}) ~ = ((VertexDomRel G) ~) \/ ({[v,w]} ~) by RELAT_1:23;
thus VertexAdjSymRel H = ((VertexDomRel G) \/ {[v,w]}) \/ ((VertexDomRel H) ~) by A2, Th27
.= ((VertexDomRel G) \/ {[v,w]}) \/ (((VertexDomRel G) \/ {[v,w]}) ~) by A2, Th27
.= ((VertexDomRel G) \/ {[v,w]}) \/ (((VertexDomRel G) ~) \/ {[w,v]}) by A6, GLIBPRE0:12
.= (((VertexDomRel G) \/ {[v,w]}) \/ {[w,v]}) \/ ((VertexDomRel G) ~) by XBOOLE_1:4
.= (((VertexDomRel G) \/ {[w,v]}) \/ {[v,w]}) \/ ((VertexDomRel G) ~) by XBOOLE_1:4
.= ((VertexDomRel G) \/ {[w,v]}) \/ (((VertexDomRel G) ~) \/ {[v,w]}) by XBOOLE_1:4
.= (VertexDomRel G) \/ (((VertexDomRel G) ~) \/ {[v,w]}) by A4, ZFMISC_1:31, XBOOLE_1:12
.= VertexAdjSymRel G by A5, ZFMISC_1:31, XBOOLE_1:12 ; :: thesis: verum
end;
end;
end;
suppose e in the_Edges_of G ; :: thesis: VertexAdjSymRel H = VertexAdjSymRel G
then G == H by GLIB_006:def 11;
hence VertexAdjSymRel H = VertexAdjSymRel G by Th49; :: thesis: verum
end;
end;