:: deftheorem Def5 defines axis URYSOHN1:def 5 :
for n being Nat
for x being Element of dyadic n
for b₃ being Nat holds
( b₃ = axis x iff x = b₃ / (2 |^ n) );