let v be Vertex of G; :: thesis: ( v is with_min_in_degree & v is with_min_out_degree implies v is with_min_degree )
assume A4: ( v is with_min_in_degree & v is with_min_out_degree ) ; :: thesis: v is with_min_degree
now :: thesis: for w being Vertex of G holds v .degree() c= w .degree()
let w be Vertex of G; :: thesis: v .degree() c= w .degree()
( v .inDegree() c= w .inDegree() & v .outDegree() c= w .outDegree() ) by A4, Th92, Th93;
hence v .degree() c= w .degree() by CARD_2:83; :: thesis: verum
end;
hence v is with_min_degree by Th36; :: thesis: verum