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