let a, b be complex number ; :: thesis: {a} -- {b} = {(a - b)}
thus {a} -- {b} = {a} ++ {(- b)} by Th25
.= {(a - b)} by Th57 ; :: thesis: verum