let r be real number ; :: 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:70;
hence 1 < 1 / r by A1, XCMPLX_0:def 7; :: thesis: verum