max X in X by Def7B;
hence max X is natural ; :: thesis: