let G be _Graph; :: thesis: for H being reverseEdgeDirections of G holds VertexDomRel H = (VertexDomRel G) ~
let H be reverseEdgeDirections of G; :: thesis: VertexDomRel H = (VertexDomRel G) ~

now :: thesis: for w, v being object holds
( ( [w,v] in (VertexDomRel G) ~ implies [w,v] in VertexDomRel H ) & ( [w,v] in VertexDomRel H implies [w,v] in (VertexDomRel G) ~ ) )

let w, v be object ; :: thesis: ( ( [w,v] in (VertexDomRel G) ~ implies [w,v] in VertexDomRel H ) & ( [w,v] in VertexDomRel H implies [w,v] in (VertexDomRel G) ~ ) )

hereby :: thesis: ( [w,v] in VertexDomRel H implies [w,v] in (VertexDomRel G) ~ )

assume [w,v] in (VertexDomRel G) ~ ; :: thesis: [w,v] in VertexDomRel H
then [v,w] in VertexDomRel G by RELAT_1:def 7;
then consider e being object such that
A1: e DJoins v,w,G by Th1;
e in the_Edges_of G by A1, GLIB_000:def 14;
then e DJoins w,v,H by A1, GLIB_007:7;
hence [w,v] in VertexDomRel H by Th1; :: thesis: verum

end;

assume [w,v] in VertexDomRel H ; :: thesis: [w,v] in (VertexDomRel G) ~
then consider e being object such that
A2: e DJoins w,v,H by Th1;
e in the_Edges_of H by A2, GLIB_000:def 14;
then e in the_Edges_of G by GLIB_007:4;
then e DJoins v,w,G by A2, GLIB_007:7;
then [v,w] in VertexDomRel G by Th1;
hence [w,v] in (VertexDomRel G) ~ by RELAT_1:def 7; :: thesis: verum

end;

hence VertexDomRel H = (VertexDomRel G) ~ by RELAT_1:def 2; :: thesis: verum