theorem :: GLIBPRE0:62

for G1, G2 being _Graph
for E being set holds
( G2 is reverseEdgeDirections of G1,E iff G2 is reverseEdgeDirections of G1,E \ (G1 .loops()) ) by Lm1, Lm2;