consider v being Vertex of G such that
A2: v .inDegree() = G .minInDegree() and
for w being Vertex of G holds v .inDegree() c= w .inDegree() by Th37;
thus G .minInDegree() is natural by A2; :: thesis: verum