theorem Th1: :: INT_3:1

for a being Element of INT.Ring holds absint . a = |.a.|