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

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