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

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

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

then reconsider n = [/r\] as Element of NAT by INT_1:3;
take n ; :: thesis: r <= n
thus r <= n by INT_1:def 7; :: thesis: verum

end;

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

take 0 ; :: thesis: r <= 0
thus r <= 0 by A1, INT_1:def 7; :: thesis: verum

end;

end;