theorem Th13: :: GLIB_007:13

for G2 being _Graph
for E, V being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v1 .edgesInOut() = v2 .edgesInOut()