x in INT by INT_1:def 2;
hence <%x%> is INT -valued ; :: thesis: verum