let G be _Graph; :: thesis: ( G is with_max_out_degree iff ex v being Vertex of G st v is with_max_out_degree )
hereby :: thesis: ( ex v being Vertex of G st v is with_max_out_degree implies G is with_max_out_degree )
assume G is with_max_out_degree ; :: thesis: ex v being Vertex of G st v is with_max_out_degree
then consider v being Vertex of G such that
A1: v .outDegree() = G .supOutDegree() and
for w being Vertex of G holds w .outDegree() c= v .outDegree() by Th81;
take v = v; :: thesis: v is with_max_out_degree
thus v is with_max_out_degree by A1; :: thesis: verum
end;
thus ( ex v being Vertex of G st v is with_max_out_degree implies G is with_max_out_degree ) by Lm5; :: thesis: verum