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