reconsider mm = m as Element of INT by INT_1:def 2;
X --> m is {mm} -valued ;
hence X --> m is INT -valued ; :: thesis: verum