theorem Th6: :: URYSOHN3:6

for x being Real st x in DYADIC holds
for n being Nat st inf_number_dyadic x <= n holds
x in dyadic n