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