theorem Th24: :: URYSOHN2:24
for a, b being Real st a < b & 0 <= a & b <= 1 holds
ex c being Real st
( c in DYADIC & a < c & c < b )