let x, y be Real; :: thesis: ( 0 < x & x < y implies ln . x < ln . y )
assume A1: ( 0 < x & x < y ) ; :: thesis: ln . x < ln . y
then A2: ( x in right_open_halfline 0 & y in right_open_halfline 0 ) by XXREAL_1:235;
number_e > 1 by XXREAL_0:2, TAYLOR_1:11;
then log (number_e,x) < log (number_e,y) by A1, POWER:57;
then (log_ number_e) . x < log (number_e,y) by A2, TAYLOR_1:def 2;
hence ln . x < ln . y by TAYLOR_1:def 3, TAYLOR_1:def 2, A2; :: thesis: verum