theorem LogMono: :: MOEBIUS3:17

for x, y being Real st 0 < x & x < y holds
ln . x < ln . y