let a, b be Complex; :: thesis: -- {a,b} = {(- a),(- b)}
thus -- {a,b} = -- ({a} \/ {b}) by ENUMSET1:1
.= (-- {a}) \/ (-- {b}) by Th15
.= {(- a)} \/ (-- {b}) by Th19
.= {(- a)} \/ {(- b)} by Th19
.= {(- a),(- b)} by ENUMSET1:1 ; :: thesis: verum