let n be Element of NAT ; :: thesis: dyadic n c= dyadic (n + 1)
let x be set ; :: 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 Element of NAT st
( 0 <= i & i <= 2 |^ (n + 1) & x = i / (2 |^ (n + 1)) )

proof

reconsider x = x as Real by A1;
consider i being Element of NAT such that
A2: ( 0 <= i & i <= 2 |^ n & x = i / (2 |^ n) ) by A1, Def3;
A4: 2 |^ (n + 1) = (2 |^ n) * 2 by NEWTON:11;
take i * 2 ; :: thesis: ( 0 <= i * 2 & i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) )
thus ( 0 <= i * 2 & i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) ) by A2, A4, XCMPLX_1:92, XREAL_1:66; :: thesis: verum

end;

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