theorem Th18: :: SURREALN:18

for r being Rational holds
( r is dyadic-like iff ex i being Integer ex n being Nat st r = i / (2 |^ n) )