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

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

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

end;

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