let G be _Graph; :: thesis: ( G is with_max_in_degree iff ex v being Vertex of G st v is with_max_in_degree )

hereby :: thesis: ( ex v being Vertex of G st v is with_max_in_degree implies G is with_max_in_degree )

assume G is with_max_in_degree ; :: thesis: ex v being Vertex of G st v is with_max_in_degree
then consider v being Vertex of G such that
A1: v .inDegree() = G .supInDegree() and
for w being Vertex of G holds w .inDegree() c= v .inDegree() by Th80;
take v = v; :: thesis: v is with_max_in_degree
thus v is with_max_in_degree by A1; :: thesis: verum

end;

thus ( ex v being Vertex of G st v is with_max_in_degree implies G is with_max_in_degree ) by Lm4; :: thesis: verum