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