let f be ExtReal; :: thesis: -- {f} = {(- f)}
let i be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not i in -- {f} or i in {(- f)} ) & ( not i in {(- f)} or i in -- {f} ) )

hereby :: thesis: ( not i in {(- f)} or i in -- {f} )

assume i in -- {f} ; :: thesis: i in {(- f)}
then consider w being Element of ExtREAL such that
A1: i = - w and
A2: w in {f} ;
w = f by A2, TARSKI:def 1;
hence i in {(- f)} by A1, TARSKI:def 1; :: thesis: verum

end;

assume i in {(- f)} ; :: thesis: i in -- {f}
then A3: i = - f by TARSKI:def 1;
( f in ExtREAL & f in {f} ) by TARSKI:def 1, XXREAL_0:def 1;
hence i in -- {f} by A3; :: thesis: verum