let G1, G2 be _Graph; :: thesis:
let F be PGraphMapping of G1,G2; :: thesis:
assume A1: ( F is directed & F is weak_SG-embedding ) ; :: thesis:
set D1 = { (v .inDegree()) where v is Vertex of G1 : verum } ;
set D2 = { (w .inDegree()) where w is Vertex of G2 : verum } ;

let x be object ; :: thesis:
assume x in G1 .supInDegree() ; :: thesis:
then consider d1 being set such that
A2: ( x in d1 & d1 in { (v .inDegree()) where v is Vertex of G1 : verum } ) by TARSKI:def 4;
consider v being Vertex of G1 such that
A3: d1 = v .inDegree() by A2;
v .inDegree() c= ((F _V) /. v) .inDegree() by A1, GLIBPRE0:88;
then A4: x in ((F _V) /. v) .inDegree() by A2, A3;
((F _V) /. v) .inDegree() in { (w .inDegree()) where w is Vertex of G2 : verum } ;
hence x in G2 .supInDegree() by A4, TARSKI:def 4; :: thesis:

end;

hence G1 .supInDegree() c= G2 .supInDegree() by TARSKI:def 3; :: thesis:
set D3 = { (v .outDegree()) where v is Vertex of G1 : verum } ;
set D4 = { (w .outDegree()) where w is Vertex of G2 : verum } ;

let x be object ; :: thesis:
assume x in G1 .supOutDegree() ; :: thesis:
then consider d1 being set such that
A5: ( x in d1 & d1 in { (v .outDegree()) where v is Vertex of G1 : verum } ) by TARSKI:def 4;
consider v being Vertex of G1 such that
A6: d1 = v .outDegree() by A5;
v .outDegree() c= ((F _V) /. v) .outDegree() by A1, GLIBPRE0:88;
then A7: x in ((F _V) /. v) .outDegree() by A5, A6;
((F _V) /. v) .outDegree() in { (w .outDegree()) where w is Vertex of G2 : verum } ;
hence x in G2 .supOutDegree() by A7, TARSKI:def 4; :: thesis:

end;