let G be _Graph; :: thesis: for c being Cardinal st ex v being Vertex of G st
( v .inDegree() = c & ( for w being Vertex of G holds w .inDegree() c= v .inDegree() ) ) holds
G .supInDegree() = c
let c be Cardinal; :: thesis: ( ex v being Vertex of G st
( v .inDegree() = c & ( for w being Vertex of G holds w .inDegree() c= v .inDegree() ) ) implies G .supInDegree() = c )
given v being Vertex of G such that A1: v .inDegree() = c and
A2: for w being Vertex of G holds w .inDegree() c= v .inDegree() ; :: thesis: G .supInDegree() = c
set S = { (v .inDegree()) where v is Vertex of G : verum } ;
c in { (v .inDegree()) where v is Vertex of G : verum } by A1;
then A3: c c= G .supInDegree() by ZFMISC_1:74;

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

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

end;

then G .supInDegree() c= c by TARSKI:def 3;
hence G .supInDegree() = c by A3, XBOOLE_0:def 10; :: thesis: verum