abs a in INT by INT_1:def 2;
hence abs a is Element of ; :: thesis: verum