theorem Th25: :: GLIB_007:25

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 & G2 is non-Dmulti & ( for e1, e2, v1, v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & not ( e1 in E & e2 in E ) holds
( not e1 in E & not e2 in E ) ) holds
G1 is non-Dmulti