theorem Cosik1: :: NUMBER18:68

for a, b being Real st a - b > 1 holds
ex t being Integer st
( a > t & t > b )