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