theorem Th4: :: DIFF_4:4

for x0, x1 being Real st x0 > 0 & x1 > 0 holds
(ln . x0) - (ln . x1) = ln . (x0 / x1)