theorem Th21: :: URYSOHN2:21

for eps being Real st 0 < eps holds
ex n being Nat st 1 < (2 |^ n) * eps