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 )
1 / (1 / r) > 1 / n by A1, A2, XREAL_1:88;
hence 1 / n < r ; :: thesis: n > 0
thus n > 0 by A1, A2; :: thesis: verum