consider v being Vertex of G such that
A1: v .outDegree() = G .supOutDegree() and
for w being Vertex of G holds w .outDegree() c= v .outDegree() by Th81;
thus G .maxOutDegree() is natural by A1; :: thesis: verum