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