let f, g be ExtReal; :: thesis: {f} /// {g} = {(f / g)}
thus {f} /// {g} = {f} ** {(g ")} by Th26
.= {(f / g)} by Th86 ; :: thesis: verum