theorem Th52: :: INT_1:54

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