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