let G be _Graph; :: thesis: ( G is with_max_out_degree implies ex v being Vertex of G st
( v .outDegree() = G .supOutDegree() & ( for w being Vertex of G holds w .outDegree() c= v .outDegree() ) ) )
assume G is with_max_out_degree ; :: thesis: ex v being Vertex of G st
( v .outDegree() = G .supOutDegree() & ( for w being Vertex of G holds w .outDegree() c= v .outDegree() ) )
then consider v being Vertex of G such that
A1: for w being Vertex of G holds w .outDegree() c= v .outDegree() ;
take v ; :: thesis: ( v .outDegree() = G .supOutDegree() & ( for w being Vertex of G holds w .outDegree() c= v .outDegree() ) )
set D = { (w .outDegree()) where w is Vertex of G : verum } ;

now :: thesis: for X being set st X in { (w .outDegree()) where w is Vertex of G : verum } holds
X c= v .outDegree()

let X be set ; :: thesis: ( X in { (w .outDegree()) where w is Vertex of G : verum } implies X c= v .outDegree() )
assume X in { (w .outDegree()) where w is Vertex of G : verum } ; :: thesis: X c= v .outDegree()
then consider w being Vertex of G such that
A2: X = w .outDegree() ;
thus X c= v .outDegree() by A1, A2; :: thesis: verum

end;

then A3: union { (w .outDegree()) where w is Vertex of G : verum } c= v .outDegree() by ZFMISC_1:76;
v .outDegree() c= G .supOutDegree() by Th35;
hence ( v .outDegree() = G .supOutDegree() & ( for w being Vertex of G holds w .outDegree() c= v .outDegree() ) ) by A1, A3, XBOOLE_0:def 10; :: thesis: verum