let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
( not m is zero & 1 / m < r ) )
assume A1: 0 < r ; :: thesis: ex m being Nat st
( not m is zero & 1 / m < r )
consider m being Nat such that
A2: 1 / r < m by SEQ_4:3;
A3: 0 < m by A1, A2;
take m ; :: thesis: ( not m is zero & 1 / m < r )
thus not m is zero by A1, A2; :: thesis: 1 / m < r
(1 / r) * r < m * r by A2, A1, XREAL_1:68;
then 1 < m * r by A1, XCMPLX_1:106;
then 1 / m < (m * r) / m by A3, XREAL_1:74;
then 1 / m < r * (m / m) by XCMPLX_1:74;
hence 1 / m < r by A3, XCMPLX_1:88; :: thesis: verum