:: deftheorem Def3 defines inf_number_dyadic URYSOHN3:def 3 :
for x being Real st x in DYADIC holds
for b₂ being Nat holds
( b₂ = inf_number_dyadic x iff ( ( x in dyadic 0 implies b₂ = 0 ) & ( b₂ = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
b₂ = n + 1 ) ) );