consider v being Vertex of G such that
A1: v .degree() = G .supDegree() and
for w being Vertex of G holds w .degree() c= v .degree() by Th79;
thus G .maxDegree() is natural by A1; :: thesis: verum