consider v being Vertex of G such that
A1: v .inDegree() = G .supInDegree() and
for w being Vertex of G holds w .inDegree() c= v .inDegree() by Th80;
thus G .maxInDegree() is natural by A1; :: thesis: verum