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)) )

proof

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;

hence x in dyadic (n + 1) by Def1; :: thesis: verum