∀x,y:{t:ℝ| r0 < t} .  (rlog((x/y)) = (rlog(x) - rlog(y))){ Auto }1. x : {t:ℝ| r0 < t} 2. y : {t:ℝ| r0 < t} ⊢ rlog((x/y)) = (rlog(x) - rlog(y))