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