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 .minDegree() c= G1 .minDegree()
let F be PGraphMapping of G1,G2; :: thesis: ( F is onto & F is semi-Dcontinuous & dom (F _V) = the_Vertices_of G1 implies G2 .minDegree() c= G1 .minDegree() )
assume A1: ( F is onto & F is semi-Dcontinuous & dom (F _V) = the_Vertices_of G1 ) ; :: thesis: G2 .minDegree() c= G1 .minDegree()
consider v1 being Vertex of G1 such that
A2: v1 .degree() = G1 .minDegree() and
for w1 being Vertex of G1 holds v1 .degree() c= w1 .degree() by Th36;
consider v2 being Vertex of G2 such that
A3: v2 .degree() = G2 .minDegree() and
A4: for w2 being Vertex of G2 holds v2 .degree() c= w2 .degree() by Th36;
A5: ((F _V) /. v1) .degree() c= v1 .degree() by A1, GLIBPRE0:91;
v2 .degree() c= ((F _V) /. v1) .degree() by A4;
hence G2 .minDegree() c= G1 .minDegree() by A2, A3, A5, XBOOLE_1:1; :: thesis: verum