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