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