consider i being Nat such that
i <= 2 |^ n and
A1: x = i / (2 |^ n) by Def1;
take i ; :: thesis: x = i / (2 |^ n)
thus x = i / (2 |^ n) by A1; :: thesis: verum