theorem Th7: :: URYSOHN3:7

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