theorem Th5: :: URYSOHN3:5

for x being Real st x in DYADIC holds
x in dyadic (inf_number_dyadic x)