let a, b be Complex; :: thesis: {a} -- {b} = {(a - b)}
thus {a} -- {b} = {a} ++ {(- b)} by Th19
.= {(a - b)} by Th51 ; :: thesis: verum