let G be locally-finite _Graph; :: thesis: for n being Nat holds
( G .minOutDegree() = n iff ex v being Vertex of G st
( v .outDegree() = n & ( for w being Vertex of G holds v .outDegree() <= w .outDegree() ) ) )
let n be Nat; :: thesis: ( G .minOutDegree() = n iff ex v being Vertex of G st
( v .outDegree() = n & ( for w being Vertex of G holds v .outDegree() <= w .outDegree() ) ) )
hereby :: thesis: ( ex v being Vertex of G st
( v .outDegree() = n & ( for w being Vertex of G holds v .outDegree() <= w .outDegree() ) ) implies G .minOutDegree() = n )
assume G .minOutDegree() = n ; :: thesis: ex v being Vertex of G st
( v .outDegree() = n & ( for w being Vertex of G holds v .outDegree() <= w .outDegree() ) )
then consider v being Vertex of G such that
A1: v .outDegree() = n and
A2: for w being Vertex of G holds v .outDegree() c= w .outDegree() by Th38;
take v = v; :: thesis: ( v .outDegree() = n & ( for w being Vertex of G holds v .outDegree() <= w .outDegree() ) )
thus v .outDegree() = n by A1; :: thesis: for w being Vertex of G holds v .outDegree() <= w .outDegree()
let w be Vertex of G; :: thesis: v .outDegree() <= w .outDegree()
Segm (v .outDegree()) c= Segm (w .outDegree()) by A2;
hence v .outDegree() <= w .outDegree() by NAT_1:39; :: thesis: verum
end;
given v being Vertex of G such that A3: v .outDegree() = n and
A4: for w being Vertex of G holds v .outDegree() <= w .outDegree() ; :: thesis: G .minOutDegree() = n
now :: 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()
Segm (v .outDegree()) c= Segm (w .outDegree()) by A4, NAT_1:39;
hence v .outDegree() c= w .outDegree() ; :: thesis: verum
end;
hence G .minOutDegree() = n by A3, Th38; :: thesis: verum