for G1 being _Graph
for G2 being Subgraph of G1 holds
( G2 .supDegree() c= G1 .supDegree() & G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() )