let G1, G2 be _Graph; for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & rng (F _V) = the_Vertices_of G2 holds
G1 .minDegree() c= G2 .minDegree()
let F be PGraphMapping of G1,G2; ( F is weak_SG-embedding & rng (F _V) = the_Vertices_of G2 implies G1 .minDegree() c= G2 .minDegree() )
assume A1:
( F is weak_SG-embedding & rng (F _V) = the_Vertices_of G2 )
; G1 .minDegree() c= G2 .minDegree()
consider v1 being Vertex of G1 such that
A2:
v1 .degree() = G1 .minDegree()
and
A3:
for w1 being Vertex of G1 holds v1 .degree() c= w1 .degree()
by Th36;
consider v2 being Vertex of G2 such that
A4:
v2 .degree() = G2 .minDegree()
and
for w2 being Vertex of G2 holds v2 .degree() c= w2 .degree()
by Th36;
consider v0 being object such that
A5:
( v0 in dom (F _V) & (F _V) . v0 = v2 )
by A1, FUNCT_1:def 3;
reconsider v0 = v0 as Vertex of G1 by A5;
v0 .degree() c= ((F _V) /. v0) .degree()
by A1, GLIBPRE0:91;
then A6:
v0 .degree() c= v2 .degree()
by A5, PARTFUN1:def 6;
v1 .degree() c= v0 .degree()
by A3;
hence
G1 .minDegree() c= G2 .minDegree()
by A2, A4, A6, XBOOLE_1:1; verum