let a, b be Complex; :: thesis: {a} /// {b} = {(a / b)}
thus {a} /// {b} = {a} ** {(b ")} by Th37
.= {(a / b)} by Th98 ; :: thesis: verum