let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is onto & F is semi-Dcontinuous & dom (F _V) = the_Vertices_of G1 holds
( G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() )
let F be PGraphMapping of G1,G2; :: thesis: ( F is onto & F is semi-Dcontinuous & dom (F _V) = the_Vertices_of G1 implies ( G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() ) )
assume A1: ( F is onto & F is semi-Dcontinuous & dom (F _V) = the_Vertices_of G1 ) ; :: thesis: ( G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() )
consider v1 being Vertex of G1 such that
A2: v1 .inDegree() = G1 .minInDegree() and
for w1 being Vertex of G1 holds v1 .inDegree() c= w1 .inDegree() by Th37;
consider v2 being Vertex of G2 such that
A3: v2 .inDegree() = G2 .minInDegree() and
A4: for w2 being Vertex of G2 holds v2 .inDegree() c= w2 .inDegree() by Th37;
A5: ((F _V) /. v1) .inDegree() c= v1 .inDegree() by A1, GLIBPRE0:92;
v2 .inDegree() c= ((F _V) /. v1) .inDegree() by A4;
hence G2 .minInDegree() c= G1 .minInDegree() by A2, A3, A5, XBOOLE_1:1; :: thesis: G2 .minOutDegree() c= G1 .minOutDegree()
consider v3 being Vertex of G1 such that
A6: v3 .outDegree() = G1 .minOutDegree() and
for w3 being Vertex of G1 holds v3 .outDegree() c= w3 .outDegree() by Th38;
consider v4 being Vertex of G2 such that
A7: v4 .outDegree() = G2 .minOutDegree() and
A8: for w4 being Vertex of G2 holds v4 .outDegree() c= w4 .outDegree() by Th38;
A9: ((F _V) /. v3) .outDegree() c= v3 .outDegree() by A1, GLIBPRE0:92;
v4 .outDegree() c= ((F _V) /. v3) .outDegree() by A8;
hence G2 .minOutDegree() c= G1 .minOutDegree() by A6, A7, A9, XBOOLE_1:1; :: thesis: verum