let a, b be complex number ; :: thesis: {a} /// {b} = {(a / b)}
thus {a} /// {b} = {a} ** {(b " )} by Th43
.= {(a / b)} by Th104 ; :: thesis: verum