let r be Real; :: thesis: ( r > 0 implies ex n being Nat st
( 1 / n < r & n > 1 ) )
assume r > 0 ; :: thesis: ex n being Nat st
( 1 / n < r & n > 1 )
then consider n being Nat such that
A1: ( 1 / n < r & n > 0 ) by FRECHET:36;
n >= 1 by A1, NAT_1:14;
then A2: n + n > 1 + 0 by XREAL_1:8;
n + n > n + 0 by A1, XREAL_1:8;
then 1 / (2 * n) < 1 / n by A1, XREAL_1:76;
then 1 / (2 * n) < r by A1, XXREAL_0:2;
hence ex n being Nat st
( 1 / n < r & n > 1 ) by A2; :: thesis: verum