for G2, G3 being _Graph
for v, e, w being object
for G1 being addEdge of G3,v,e,w st not e in the_Edges_of G3 holds
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )