let a, b be Real; :: thesis: ( 0 < a & a < b implies b " < a " )
A1: b " = 1 / b by XCMPLX_1:215;
assume that
A2: 0 < a and
A3: a < b ; :: thesis: b " < a "
a * (b ") < b * (b ") by A2, A3, Lm13;
then a * (b ") < 1 by A1, A2, A3, XCMPLX_1:87;
then (a ") * (a * (b ")) < 1 * (a ") by A2, Lm13;
then ((a ") * a) * (b ") < 1 * (a ") ;
then 1 * (b ") < 1 * (a ") by A2, XCMPLX_0:def 7;
hence b " < a " ; :: thesis: verum