theorem :: GLIB_009:51
for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds G1 .loops() = G2 .loops()