let G be _Graph; :: thesis: for c being Cardinal holds
( G .minOutDegree() = c iff ex v being Vertex of G st
( v .outDegree() = c & ( for w being Vertex of G holds v .outDegree() c= w .outDegree() ) ) )
let c be Cardinal; :: thesis: ( G .minOutDegree() = c iff ex v being Vertex of G st
( v .outDegree() = c & ( for w being Vertex of G holds v .outDegree() c= w .outDegree() ) ) )
set S = { (v .outDegree()) where v is Vertex of G : verum } ;
the Vertex of G .outDegree() in { (v .outDegree()) where v is Vertex of G : verum } ;
then A1: { (v .outDegree()) where v is Vertex of G : verum } <> {} ;
now :: thesis: for x being set st x in { (v .outDegree()) where v is Vertex of G : verum } holds
x is cardinal number
let x be set ; :: thesis: ( x in { (v .outDegree()) where v is Vertex of G : verum } implies x is cardinal number )
assume x in { (v .outDegree()) where v is Vertex of G : verum } ; :: thesis: x is cardinal number
then consider v being Vertex of G such that
A2: x = v .outDegree() ;
thus x is cardinal number by A2; :: thesis: verum
end;
then consider A being Cardinal such that
A3: ( A in { (v .outDegree()) where v is Vertex of G : verum } & A = G .minOutDegree() ) by A1, GLIBPRE0:14;
hereby :: thesis: ( ex v being Vertex of G st
( v .outDegree() = c & ( for w being Vertex of G holds v .outDegree() c= w .outDegree() ) ) implies G .minOutDegree() = c )
assume A4: G .minOutDegree() = c ; :: thesis: ex v being Vertex of G st
( v .outDegree() = c & ( for w being Vertex of G holds v .outDegree() c= w .outDegree() ) )
consider v being Vertex of G such that
A5: A = v .outDegree() by A3;
take v = v; :: thesis: ( v .outDegree() = c & ( for w being Vertex of G holds v .outDegree() c= w .outDegree() ) )
thus v .outDegree() = c by A4, A3, A5; :: thesis: for w being Vertex of G holds v .outDegree() c= w .outDegree()
let w be Vertex of G; :: thesis: v .outDegree() c= w .outDegree()
w .outDegree() in { (v .outDegree()) where v is Vertex of G : verum } ;
hence v .outDegree() c= w .outDegree() by A3, A5, SETFAM_1:3; :: thesis: verum
end;
given v being Vertex of G such that A6: v .outDegree() = c and
A7: for w being Vertex of G holds v .outDegree() c= w .outDegree() ; :: thesis: G .minOutDegree() = c
c in { (v .outDegree()) where v is Vertex of G : verum } by A6;
then A8: G .minOutDegree() c= c by SETFAM_1:3;
now :: thesis: for x being object st x in c holds
x in meet { (v .outDegree()) where v is Vertex of G : verum }
let x be object ; :: thesis: ( x in c implies x in meet { (v .outDegree()) where v is Vertex of G : verum } )
assume A9: x in c ; :: thesis: x in meet { (v .outDegree()) where v is Vertex of G : verum }
now :: thesis: for X being set st X in { (v .outDegree()) where v is Vertex of G : verum } holds
x in X
let X be set ; :: thesis: ( X in { (v .outDegree()) where v is Vertex of G : verum } implies x in X )
assume X in { (v .outDegree()) where v is Vertex of G : verum } ; :: thesis: x in X
then consider w being Vertex of G such that
A10: X = w .outDegree() ;
c c= X by A6, A7, A10;
hence x in X by A9; :: thesis: verum
end;
hence x in meet { (v .outDegree()) where v is Vertex of G : verum } by A1, SETFAM_1:def 1; :: thesis: verum
end;
then c c= G .minOutDegree() by TARSKI:def 3;
hence G .minOutDegree() = c by A8, XBOOLE_0:def 10; :: thesis: verum