let n be Nat; :: thesis: dyadic n c= dyadic (n + 1)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dyadic n or x in dyadic (n + 1) )

assume A1: x in dyadic n ; :: thesis: x in dyadic (n + 1)

ex i being Nat st

( i <= 2 |^ (n + 1) & x = i / (2 |^ (n + 1)) )

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dyadic n or x in dyadic (n + 1) )

assume A1: x in dyadic n ; :: thesis: x in dyadic (n + 1)

ex i being Nat st

( i <= 2 |^ (n + 1) & x = i / (2 |^ (n + 1)) )

proof

hence
x in dyadic (n + 1)
by Def1; :: thesis: verum
reconsider x = x as Real by A1;

consider i being Nat such that

A2: ( i <= 2 |^ n & x = i / (2 |^ n) ) by A1, Def1;

take i * 2 ; :: thesis: ( i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) )

2 |^ (n + 1) = (2 |^ n) * 2 by NEWTON:6;

hence ( i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) ) by A2, XCMPLX_1:91, XREAL_1:64; :: thesis: verum

end;consider i being Nat such that

A2: ( i <= 2 |^ n & x = i / (2 |^ n) ) by A1, Def1;

take i * 2 ; :: thesis: ( i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) )

2 |^ (n + 1) = (2 |^ n) * 2 by NEWTON:6;

hence ( i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) ) by A2, XCMPLX_1:91, XREAL_1:64; :: thesis: verum