@ x is INT -valued by HILB10_2:def 1;
hence eval (p,(@ x)) is integer ; :: thesis: verum