consider v being Vertex of G such that
A3: v .outDegree() = G .minOutDegree() and
for w being Vertex of G holds v .outDegree() c= w .outDegree() by Th38;
take v ; :: thesis: v is with_min_out_degree
thus v is with_min_out_degree by A3; :: thesis: verum