let r be Real; :: thesis: ( r > 0 implies ex n being Nat st

( 1 / n < r & n > 0 ) )

assume A1: r > 0 ; :: thesis: ex n being Nat st

( 1 / n < r & n > 0 )

consider n being Nat such that

A2: 1 / r < n by SEQ_4:3;

take n ; :: thesis: ( 1 / n < r & n > 0 )

SS: ( r " = 1 / r & n " = 1 / n ) by XCMPLX_1:215;

(r ") " > n " by A2, SS, A1, XREAL_1:88;

hence 1 / n < r by XCMPLX_1:215; :: thesis: n > 0

thus n > 0 by A1, A2; :: thesis: verum

( 1 / n < r & n > 0 ) )

assume A1: r > 0 ; :: thesis: ex n being Nat st

( 1 / n < r & n > 0 )

consider n being Nat such that

A2: 1 / r < n by SEQ_4:3;

take n ; :: thesis: ( 1 / n < r & n > 0 )

SS: ( r " = 1 / r & n " = 1 / n ) by XCMPLX_1:215;

(r ") " > n " by A2, SS, A1, XREAL_1:88;

hence 1 / n < r by XCMPLX_1:215; :: thesis: n > 0

thus n > 0 by A1, A2; :: thesis: verum