let eps be Real; :: thesis: ( 0 < eps implies ex n being Nat st 1 < (2 |^ n) * eps )
assume A1: 0 < eps ; :: thesis: ex n being Nat st 1 < (2 |^ n) * eps
consider n being Nat such that
A2: 1 / eps < n by SEQ_4:3;
take n ; :: thesis: 1 < (2 |^ n) * eps
n < 2 |^ n by NEWTON:86;
then 1 / eps < 2 |^ n by A2, XXREAL_0:2;
then (1 / eps) * eps < (2 |^ n) * eps by A1, XREAL_1:68;
hence 1 < (2 |^ n) * eps by A1, XCMPLX_1:87; :: thesis: verum