for G being _Graph holds G is reverseEdgeDirections of G, {} by Th42;