let G2 be _Graph; :: thesis: for G1 being reverseEdgeDirections of G2 holds G2 is reverseEdgeDirections of G1
let G1 be reverseEdgeDirections of G2; :: thesis: G2 is reverseEdgeDirections of G1
the_Edges_of G1 = the_Edges_of G2 by Th4;
hence G2 is reverseEdgeDirections of G1 by Th3; :: thesis: verum