let f, g be ext-real number ; :: thesis: -- {f,g} = {(- f),(- g)}
thus -- {f,g} = -- ({f} \/ {g}) by ENUMSET1:41
.= (-- {f}) \/ (-- {g}) by Th11
.= {(- f)} \/ (-- {g}) by Th15
.= {(- f)} \/ {(- g)} by Th15
.= {(- f),(- g)} by ENUMSET1:41 ; :: thesis: verum