theorem Th4: :: CARDFIN2:4

for a being Integer
for b being Real st |.(a - b).| < 1 / 2 holds
a = round b