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
0 < r " by A1;
then 1 * (r " ) > r * (r " ) by A2, XREAL_1:70;
then (1 " ) * (1 * (r " )) > (1 " ) * 1 by A1, XCMPLX_0:def 7;
hence 1 < 1 / r ; :: thesis: verum