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