let G1 be _Graph; :: thesis: for G2 being spanning Subgraph of G1 holds
( G2 .minDegree() c= G1 .minDegree() & G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() )
let G2 be spanning Subgraph of G1; :: thesis: ( G2 .minDegree() c= G1 .minDegree() & G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() )
set F = (id G1) | G2;
A1: ( (id G1) | G2 is directed & (id G1) | G2 is weak_SG-embedding ) by GLIB_010:57;
rng (((id G1) | G2) _V) = rng (((id G1) _V) | (the_Vertices_of G1)) by GLIB_000:def 33
.= the_Vertices_of G1 ;
hence ( G2 .minDegree() c= G1 .minDegree() & G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() ) by A1, Th52, Th57; :: thesis: verum