let G be _Graph; :: thesis: for v, w being Vertex of G st v is with_min_out_degree holds
v .outDegree() c= w .outDegree()
let v, w be Vertex of G; :: thesis: ( v is with_min_out_degree implies v .outDegree() c= w .outDegree() )
assume v is with_min_out_degree ; :: thesis: v .outDegree() c= w .outDegree()
then v .outDegree() = G .minOutDegree() ;
then consider v0 being Vertex of G such that
A1: v0 .outDegree() = v .outDegree() and
A2: for u being Vertex of G holds v0 .outDegree() c= u .outDegree() by Th38;
thus v .outDegree() c= w .outDegree() by A1, A2; :: thesis: verum