theorem Th7: :: GLIB_007:7

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & e in E holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )