let r be Real; :: thesis: ( r > 0 implies ex n being Nat st
( n > 0 & 1 / n < r ) )
assume A1: r > 0 ; :: thesis: ex n being Nat st
( n > 0 & 1 / n < r )
A2: 1 / r > 0 by A1;
consider n being Nat such that
A3: 1 / r < n by SEQ_4:3;
(1 / r) * r < n * r by A1, A3, XREAL_1:68;
then 1 < n * r by A1, XCMPLX_1:87;
then 1 / n < r by A3, A2, XREAL_1:83;
hence ex n being Nat st
( n > 0 & 1 / n < r ) by A3, A2; :: thesis: verum