let r be Real; :: thesis: ( r > 0 implies ex n being Element of NAT st
( n > 0 & 1 / n < r ) )
assume A1: r > 0 ; :: thesis: ex n being Element of NAT st
( n > 0 & 1 / n < r )
consider n being Element of NAT such that
A2: 1 / r < n by SEQ_4:10;
A3: 1 / r > 0 by A1;
(1 / r) * r < n * r by A1, A2, XREAL_1:70;
then 1 < n * r by A1, XCMPLX_1:88;
then 1 / n < r by A2, A3, XREAL_1:85;
hence ex n being Element of NAT st
( n > 0 & 1 / n < r ) by A2, A3; :: thesis: verum