let G be _Graph; :: thesis: for c being Cardinal holds
( G .minDegree() = c iff ex v being Vertex of G st
( v .degree() = c & ( for w being Vertex of G holds v .degree() c= w .degree() ) ) )
let c be Cardinal; :: thesis: ( G .minDegree() = c iff ex v being Vertex of G st
( v .degree() = c & ( for w being Vertex of G holds v .degree() c= w .degree() ) ) )
set S = { (v .degree()) where v is Vertex of G : verum } ;
the Vertex of G .degree() in { (v .degree()) where v is Vertex of G : verum } ;
then A1: { (v .degree()) where v is Vertex of G : verum } <> {} ;

now :: thesis: for x being set st x in { (v .degree()) where v is Vertex of G : verum } holds
x is cardinal number

let x be set ; :: thesis: ( x in { (v .degree()) where v is Vertex of G : verum } implies x is cardinal number )
assume x in { (v .degree()) where v is Vertex of G : verum } ; :: thesis: x is cardinal number
then consider v being Vertex of G such that
A2: x = v .degree() ;
thus x is cardinal number by A2; :: thesis: verum

end;

then consider A being Cardinal such that
A3: ( A in { (v .degree()) where v is Vertex of G : verum } & A = G .minDegree() ) by A1, GLIBPRE0:14;

hereby :: thesis: ( ex v being Vertex of G st
( v .degree() = c & ( for w being Vertex of G holds v .degree() c= w .degree() ) ) implies G .minDegree() = c )

assume A4: G .minDegree() = c ; :: thesis: ex v being Vertex of G st
( v .degree() = c & ( for w being Vertex of G holds v .degree() c= w .degree() ) )
consider v being Vertex of G such that
A5: A = v .degree() by A3;
take v = v; :: thesis: ( v .degree() = c & ( for w being Vertex of G holds v .degree() c= w .degree() ) )
thus v .degree() = c by A4, A3, A5; :: thesis: for w being Vertex of G holds v .degree() c= w .degree()
let w be Vertex of G; :: thesis: v .degree() c= w .degree()
w .degree() in { (v .degree()) where v is Vertex of G : verum } ;
hence v .degree() c= w .degree() by A3, A5, SETFAM_1:3; :: thesis: verum

end;

given v being Vertex of G such that A6: v .degree() = c and
A7: for w being Vertex of G holds v .degree() c= w .degree() ; :: thesis: G .minDegree() = c
c in { (v .degree()) where v is Vertex of G : verum } by A6;
then A8: G .minDegree() c= c by SETFAM_1:3;

now :: thesis: for x being object st x in c holds
x in meet { (v .degree()) where v is Vertex of G : verum }

let x be object ; :: thesis: ( x in c implies x in meet { (v .degree()) where v is Vertex of G : verum } )
assume A9: x in c ; :: thesis: x in meet { (v .degree()) where v is Vertex of G : verum }

now :: thesis: for X being set st X in { (v .degree()) where v is Vertex of G : verum } holds
x in X

let X be set ; :: thesis: ( X in { (v .degree()) where v is Vertex of G : verum } implies x in X )
assume X in { (v .degree()) where v is Vertex of G : verum } ; :: thesis: x in X
then consider w being Vertex of G such that
A10: X = w .degree() ;
c c= X by A6, A7, A10;
hence x in X by A9; :: thesis: verum

end;

hence x in meet { (v .degree()) where v is Vertex of G : verum } by A1, SETFAM_1:def 1; :: thesis: verum

end;

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