let r be Real; :: thesis: ex n being Element of NAT st r <= n

per cases ( [/r\] >= 0 or [/r\] < 0 ) ;

suppose A1: [/r\] >= 0 ; :: thesis: ex n being Element of NAT st r <= n

reconsider n = [/r\] as Element of NAT by A1, INT_1:16;
take n ; :: thesis: r <= n
thus r <= n by INT_1:def 5; :: thesis: verum

end;

suppose A2: [/r\] < 0 ; :: thesis: ex n being Element of NAT st r <= n

take 0 ; :: thesis: r <= 0
thus r <= 0 by A2, INT_1:def 5; :: thesis: verum

end;

end;