let G be _Graph; :: thesis: for E being set
for H being reverseEdgeDirections of G,E holds VertexAdjSymRel H = VertexAdjSymRel G
let E be set ; :: thesis: for H being reverseEdgeDirections of G,E holds VertexAdjSymRel H = VertexAdjSymRel G
let H be reverseEdgeDirections of G,E; :: thesis: VertexAdjSymRel H = VertexAdjSymRel G
now :: thesis: for v, w being object holds
( ( [v,w] in VertexAdjSymRel G implies [v,w] in VertexAdjSymRel H ) & ( [v,w] in VertexAdjSymRel H implies [v,w] in VertexAdjSymRel G ) )
let v, w be object ; :: thesis: ( ( [v,w] in VertexAdjSymRel G implies [v,w] in VertexAdjSymRel H ) & ( [v,w] in VertexAdjSymRel H implies [v,w] in VertexAdjSymRel G ) )
hereby :: thesis: ( [v,w] in VertexAdjSymRel H implies [v,w] in VertexAdjSymRel G )
assume [v,w] in VertexAdjSymRel G ; :: thesis: [v,w] in VertexAdjSymRel H
then consider e being object such that
A1: e Joins v,w,G by Th32;
e Joins v,w,H by A1, GLIB_007:9;
hence [v,w] in VertexAdjSymRel H by Th32; :: thesis: verum
end;
assume [v,w] in VertexAdjSymRel H ; :: thesis: [v,w] in VertexAdjSymRel G
then consider e being object such that
A2: e Joins v,w,H by Th32;
e Joins v,w,G by A2, GLIB_007:9;
hence [v,w] in VertexAdjSymRel G by Th32; :: thesis: verum
end;
hence VertexAdjSymRel H = VertexAdjSymRel G by RELAT_1:def 2; :: thesis: verum