let G1, G2 be _Graph; :: thesis:
let F be PGraphMapping of G1,G2; :: thesis:
assume A1: ( F is directed & F is weak_SG-embedding & rng (F _V) = the_Vertices_of G2 ) ; :: thesis:
consider v1 being Vertex of G1 such that
A2: v1 .inDegree() = G1 .minInDegree() and
A3: for w1 being Vertex of G1 holds v1 .inDegree() c= w1 .inDegree() by Th37;
consider v2 being Vertex of G2 such that
A4: v2 .inDegree() = G2 .minInDegree() and
for w2 being Vertex of G2 holds v2 .inDegree() c= w2 .inDegree() by Th37;
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 .inDegree() c= ((F _V) /. v0) .inDegree() by A1, GLIBPRE0:88;
then A6: v0 .inDegree() c= v2 .inDegree() by A5, PARTFUN1:def 6;
v1 .inDegree() c= v0 .inDegree() by A3;
hence G1 .minInDegree() c= G2 .minInDegree() by A2, A4, A6, XBOOLE_1:1; :: thesis:
consider v3 being Vertex of G1 such that
A7: v3 .outDegree() = G1 .minOutDegree() and
A8: for w3 being Vertex of G1 holds v3 .outDegree() c= w3 .outDegree() by Th38;
consider v4 being Vertex of G2 such that
A9: v4 .outDegree() = G2 .minOutDegree() and
for w4 being Vertex of G2 holds v4 .outDegree() c= w4 .outDegree() by Th38;
consider v9 being object such that
A10: ( v9 in dom (F _V) & (F _V) . v9 = v4 ) by A1, FUNCT_1:def 3;
reconsider v9 = v9 as Vertex of G1 by A10;
v9 .outDegree() c= ((F _V) /. v9) .outDegree() by A1, GLIBPRE0:88;
then A11: v9 .outDegree() c= v4 .outDegree() by A10, PARTFUN1:def 6;
v3 .outDegree() c= v9 .outDegree() by A8;
hence G1 .minOutDegree() c= G2 .minOutDegree() by A7, A9, A11, XBOOLE_1:1; :: thesis: