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