let r be Real; :: thesis: ( 0 < r & r < 1 implies 1 < 1 / r )
assume that
A1: 0 < r and
A2: r < 1 ; :: thesis: 1 < 1 / r
1 * (r ") > r * (r ") by A1, A2, XREAL_1:68;
hence 1 < 1 / r by A1, XCMPLX_0:def 7; :: thesis: verum