let G1 be _Graph; :: thesis: for G2 being Subgraph of G1 holds
( G2 .supDegree() c= G1 .supDegree() & G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() )
let G2 be Subgraph of G1; :: thesis: ( G2 .supDegree() c= G1 .supDegree() & G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() )
set F = (id G1) | G2;
( (id G1) | G2 is directed & (id G1) | G2 is weak_SG-embedding ) by GLIB_010:57;
hence ( G2 .supDegree() c= G1 .supDegree() & G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() ) by Th51, Th56; :: thesis: verum