let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is onto & F is semi-Dcontinuous holds
( G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() )
let F be PGraphMapping of G1,G2; :: thesis: ( F is onto & F is semi-Dcontinuous implies ( G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() ) )
assume A1: ( F is onto & F is semi-Dcontinuous ) ; :: thesis: ( G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() )
set D1 = { (v .inDegree()) where v is Vertex of G1 : verum } ;
set D2 = { (w .inDegree()) where w is Vertex of G2 : verum } ;

now :: thesis: for x being object st x in G2 .supInDegree() holds
x in G1 .supInDegree()

let x be object ; :: thesis: ( x in G2 .supInDegree() implies x in G1 .supInDegree() )
assume x in G2 .supInDegree() ; :: thesis: x in G1 .supInDegree()
then consider d2 being set such that
A2: ( x in d2 & d2 in { (w .inDegree()) where w is Vertex of G2 : verum } ) by TARSKI:def 4;
consider w being Vertex of G2 such that
A3: d2 = w .inDegree() by A2;
rng (F _V) = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v being object such that
A4: ( v in dom (F _V) & (F _V) . v = w ) by FUNCT_1:def 3;
reconsider v = v as Vertex of G1 by A4;
((F _V) /. v) .inDegree() c= v .inDegree() by A1, A4, GLIBPRE0:90;
then w .inDegree() c= v .inDegree() by A4, PARTFUN1:def 6;
then A5: x in v .inDegree() by A2, A3;
v .inDegree() in { (v .inDegree()) where v is Vertex of G1 : verum } ;
hence x in G1 .supInDegree() by A5, TARSKI:def 4; :: thesis: verum

end;

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

now :: thesis: for x being object st x in G2 .supOutDegree() holds
x in G1 .supOutDegree()

let x be object ; :: thesis: ( x in G2 .supOutDegree() implies x in G1 .supOutDegree() )
assume x in G2 .supOutDegree() ; :: thesis: x in G1 .supOutDegree()
then consider d2 being set such that
A6: ( x in d2 & d2 in { (w .outDegree()) where w is Vertex of G2 : verum } ) by TARSKI:def 4;
consider w being Vertex of G2 such that
A7: d2 = w .outDegree() by A6;
rng (F _V) = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v being object such that
A8: ( v in dom (F _V) & (F _V) . v = w ) by FUNCT_1:def 3;
reconsider v = v as Vertex of G1 by A8;
((F _V) /. v) .outDegree() c= v .outDegree() by A1, A8, GLIBPRE0:90;
then w .outDegree() c= v .outDegree() by A8, PARTFUN1:def 6;
then A9: x in v .outDegree() by A6, A7;
v .outDegree() in { (v .outDegree()) where v is Vertex of G1 : verum } ;
hence x in G1 .supOutDegree() by A9, TARSKI:def 4; :: thesis: verum

end;

hence G2 .supOutDegree() c= G1 .supOutDegree() by TARSKI:def 3; :: thesis: verum