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