let G be _Graph; :: thesis: ( ex v being Vertex of G st v .inDegree() = G .supInDegree() implies G is with_max_in_degree )
given v being Vertex of G such that A1: v .inDegree() = G .supInDegree() ; :: thesis: G is with_max_in_degree
for w being Vertex of G holds w .inDegree() c= v .inDegree() by A1, Th35;
hence G is with_max_in_degree ; :: thesis: verum