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