now :: thesis: ex v being Vertex of G st
( v .outDegree() = 0 & ( for w being Vertex of G holds w .outDegree() c= v .outDegree() ) )

take v = the Vertex of G; :: thesis: ( v .outDegree() = 0 & ( for w being Vertex of G holds w .outDegree() c= v .outDegree() ) )
thus v .outDegree() = 0 ; :: thesis: for w being Vertex of G holds w .outDegree() c= v .outDegree()
let w be Vertex of G; :: thesis: w .outDegree() c= v .outDegree()
thus w .outDegree() c= v .outDegree() ; :: thesis: verum

end;

hence G .supOutDegree() is zero by Th50; :: thesis: verum