max X in X by Def8;
hence max X is natural ; :: thesis: verum