theorem :: GLIB_013:61
for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() )