{ (- w) where w is Element of ExtREAL : w in F } is ext-real-membered
proof
let e be object ; :: according to MEMBERED:def 2 :: thesis: ( not e in { (- w) where w is Element of ExtREAL : w in F } or e is ext-real )
assume e in { (- w) where w is Element of ExtREAL : w in F } ; :: thesis: e is ext-real
then ex w being Element of ExtREAL st
( e = - w & w in F ) ;
hence e is ext-real ; :: thesis: verum
end;
hence { (- w) where w is Element of ExtREAL : w in F } is ext-real-membered set ; :: thesis: verum