let a, b be real number ; :: thesis: ( 0 < a & a < b implies b " < a " )
A1: ( b " = 1 / b & a " = 1 / a ) by XCMPLX_1:217;
assume A2: ( 0 < a & a < b ) ; :: thesis: b " < a "
a * (b " ) < b * (b " ) by A2, Lm13;
then A3: a * (b " ) < 1 by A1, A2, XCMPLX_1:88;
a " > 0 by A2;
then (a " ) * (a * (b " )) < 1 * (a " ) by A3, Lm13;
then ((a " ) * a) * (b " ) < 1 * (a " ) ;
then 1 * (b " ) < 1 * (a " ) by A2, XCMPLX_0:def 7;
hence b " < a " ; :: thesis: verum