for G1 being _Graph
for G2 being spanning Subgraph of G1 holds
( G2 .minDegree() c= G1 .minDegree() & G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() )