let A be positive Real; :: thesis: ex n being positive Nat st 1 / (2 |^ n) <= A
consider n being positive Nat such that
A1: 1 / A <= 2 |^ n by Th2;
take n ; :: thesis: 1 / (2 |^ n) <= A
1 / (1 / A) >= 1 / (2 |^ n) by A1, XREAL_1:118;
hence 1 / (2 |^ n) <= A ; :: thesis: verum