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

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

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

end;

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

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

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

end;

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

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

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

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

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

end;

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

end;

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