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;
take v ; :: thesis: v is with_min_degree
thus v is with_min_degree by A1; :: thesis: verum