let F be ext-real-membered set ; :: thesis: -- (F "" ) = (-- F) ""
let i be ext-real number ; :: 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 - i in F "" by Th8;
then consider w being Element of ExtREAL such that
A1: - i = w " and
A2: w in F ;
A3: (- w) " = - (w " ) by XXREAL_3:111;
- w in -- F by A2;
hence i in (-- F) "" by A1, A3; :: thesis: verum

end;

assume i in (-- F) "" ; :: thesis: i in -- (F "" )
then consider w being Element of ExtREAL such that
A4: i = w " and
A5: w in -- F ;
A6: (- w) " = - (w " ) by XXREAL_3:111;
- w in F by A5, Th8;
then - i in F "" by A4, A6;
hence i in -- (F "" ) by Th8; :: thesis: verum