let f, g be ExtReal; :: thesis: -- {f,g} = {(- f),(- g)}
thus -- {f,g} = -- ({f} \/ {g}) by ENUMSET1:1
.= (-- {f}) \/ (-- {g}) by Th5
.= {(- f)} \/ (-- {g}) by Th9
.= {(- f)} \/ {(- g)} by Th9
.= {(- f),(- g)} by ENUMSET1:1 ; :: thesis: verum