theorem :: INT_1:65

for i being Integer
for r being Real st r <= i holds
[/r\] <= i