let p be Real; :: thesis: ( p > 0 implies ex k being Nat st 1 / (k + 1) < p )
consider k1 being Nat such that
A1: p " < k1 by SEQ_4:3;
assume p > 0 ; :: thesis: ex k being Nat st 1 / (k + 1) < p
then A2: 0 < p " ;
take k1 ; :: thesis: 1 / (k1 + 1) < p
(p ") + 0 < k1 + 1 by A1, XREAL_1:8;
then 1 / (k1 + 1) < 1 / (p ") by A2, XREAL_1:76;
hence 1 / (k1 + 1) < p by XCMPLX_1:216; :: thesis: verum