min X in X by Def7;
hence min X is integer ; :: thesis: verum