let a be Real; :: thesis: ( 1 < a implies a " < 1 )
assume A1: 1 < a ; :: thesis: a " < 1
then 1 * (a ") < a * (a ") by Lm13;
hence a " < 1 by A1, XCMPLX_0:def 7; :: thesis: verum