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

( 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