theorem Th22: :: URYSOHN2:22

for a, b being Real st 0 <= a & 1 < b - a holds
ex n being Nat st
( a < n & n < b )