min X in X by Def7;
hence min X is natural ; :: thesis: