for n being Nat
for x being Real st x in dyadic n holds
( 0 <= x & x <= 1 )