theorem Th1: :: URYSOHN1:1

for n being Nat
for x being Real st x in dyadic n holds
( 0 <= x & x <= 1 )