let p be real number ; :: thesis: ( p > 0 implies ex k being Element of NAT st 1 / (k + 1) < p )
assume p > 0 ; :: thesis: ex k being Element of NAT st 1 / (k + 1) < p
then A1: 0 < p " by XREAL_1:124;
consider k1 being Element of NAT such that
A2: p " < k1 by SEQ_4:10;
take k = k1; :: thesis: 1 / (k + 1) < p
(p " ) + 0 < k1 + 1 by A2, XREAL_1:10;
then 1 / (k1 + 1) < 1 / (p " ) by A1, XREAL_1:78;
hence 1 / (k + 1) < p by XCMPLX_1:218; :: thesis: verum