let a, s, t be complex number ; :: thesis: {a} -- {s,t} = {(a - s),(a - t)}
thus {a} -- {s,t} = {a} ++ {(- s),(- t)} by Th26
.= {(a - s),(a - t)} by Th58 ; :: thesis: verum