for G2 being _Graph
for G1 being reverseEdgeDirections of G2 holds G2 is reverseEdgeDirections of G1