let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
G1 .supDegree() c= G2 .supDegree()
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding implies G1 .supDegree() c= G2 .supDegree() )
assume A1: F is weak_SG-embedding ; :: thesis: G1 .supDegree() c= G2 .supDegree()
set D1 = { (v .degree()) where v is Vertex of G1 : verum } ;
set D2 = { (w .degree()) where w is Vertex of G2 : verum } ;

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

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

end;

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