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