let a be Element of INT.Ring ; :: thesis: absint . a = abs a
reconsider a9 = a as Integer ;
absint . a = absreal . a9 by Def6
.= abs a9 by EUCLID:def 2 ;
hence absint . a = abs a ; :: thesis: verum