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