theorem Th1: :: DIFF_4:1

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