let a be Integer; :: thesis: ( a = 0 or absreal . a >= 1 )
assume A1: a <> 0 ; :: thesis: absreal . a >= 1

now

per cases ( 0 <= a or a < 0 ) ;

case 0 <= a ; :: thesis: absreal . a >= 1

then reconsider a = a as Element of NAT by INT_1:16;
A3: absreal . a = abs a by EUCLID:def 2
.= a by ABSVALUE:def 1 ;
0 + 1 < a + 1 by A1, XREAL_1:8;
hence absreal . a >= 1 by A3, NAT_1:13; :: thesis: verum

end;

case A4: a < 0 ; :: thesis: absreal . a >= 1

A5: absreal . a = abs a by EUCLID:def 2
.= - a by A4, ABSVALUE:def 1 ;
a <= - 1 by A4, INT_1:21;
then - (- 1) <= - a by XREAL_1:26;
hence absreal . a >= 1 by A5; :: thesis: verum

end;

end;

end;

hence absreal . a >= 1 ; :: thesis: verum