let F be ext-real-membered set ; :: thesis: for f being ExtReal holds F -- f = { (w - f) where w is Element of ExtREAL : w in F }
let f be ExtReal; :: thesis: F -- f = { (w - f) where w is Element of ExtREAL : w in F }
thus F -- f c= { (w - f) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def 10 :: thesis: { (w - f) where w is Element of ExtREAL : w in F } c= F -- f

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in F -- f or e in { (w - f) where w is Element of ExtREAL : w in F } )
assume e in F -- f ; :: thesis: e in { (w - f) where w is Element of ExtREAL : w in F }
then consider w1, w2 being Element of ExtREAL such that
A1: ( e = w1 + w2 & w1 in F ) and
A2: w2 in -- {f} ;
- w2 in {f} by A2, Th2;
then ( w1 - (- w2) = w1 + w2 & - w2 = f ) by TARSKI:def 1;
hence e in { (w - f) where w is Element of ExtREAL : w in F } by A1; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (w - f) where w is Element of ExtREAL : w in F } or e in F -- f )
assume e in { (w - f) where w is Element of ExtREAL : w in F } ; :: thesis: e in F -- f
then ex w being Element of ExtREAL st
( e = w - f & w in F ) ;
hence e in F -- f by Th168; :: thesis: verum