theorem :: DIFF_4:30

for x0, x1 being Real st x0 > 0 & x1 > 0 holds
[!ln,x0,x1!] = (ln . (x0 / x1)) / (x0 - x1) by Th4;