let A, B be ext-real-membered set ; :: thesis: ( A = { (- w) where w is Element of ExtREAL : w in B } implies B = { (- w) where w is Element of ExtREAL : w in A } )
assume A1: A = { (- w) where w is Element of ExtREAL : w in B } ; :: thesis: B = { (- w) where w is Element of ExtREAL : w in A }
thus B c= { (- w) where w is Element of ExtREAL : w in A } :: according to XBOOLE_0:def 10 :: thesis: { (- w) where w is Element of ExtREAL : w in A } c= B

proof

let z be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not z in B or z in { (- w) where w is Element of ExtREAL : w in A } )
A2: z in ExtREAL by XXREAL_0:def 1;
A3: ( - z in ExtREAL & z = - (- z) ) by XXREAL_0:def 1;
assume z in B ; :: thesis: z in { (- w) where w is Element of ExtREAL : w in A }
then - z in A by A1, A2;
hence z in { (- w) where w is Element of ExtREAL : w in A } by A3; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (- w) where w is Element of ExtREAL : w in A } or e in B )
assume e in { (- w) where w is Element of ExtREAL : w in A } ; :: thesis: e in B
then consider w1 being Element of ExtREAL such that
A4: - w1 = e and
A5: w1 in A ;
ex w being Element of ExtREAL st
( - w = w1 & w in B ) by A1, A5;
hence e in B by A4; :: thesis: verum