let G be _Graph; :: thesis: G .supInDegree() c= G .supDegree()

now :: thesis: for x being object st x in G .supInDegree() holds
x in G .supDegree()

let x be object ; :: thesis: ( x in G .supInDegree() implies x in G .supDegree() )
assume x in G .supInDegree() ; :: thesis: x in G .supDegree()
then consider X being set such that
A1: ( x in X & X in { (v .inDegree()) where v is Vertex of G : verum } ) by TARSKI:def 4;
consider v being Vertex of G such that
A2: X = v .inDegree() by A1;
v .inDegree() c= v .degree() by CARD_2:94;
then A3: x in v .degree() by A1, A2;
v .degree() in { (w .degree()) where w is Vertex of G : verum } ;
hence x in G .supDegree() by A3, TARSKI:def 4; :: thesis: verum

end;

hence G .supInDegree() c= G .supDegree() by TARSKI:def 3; :: thesis: verum