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