let F be ext-real-membered set ; :: thesis: for f being ExtReal holds f -- F = { (f - w) where w is Element of ExtREAL : w in F }
let f be ExtReal; :: thesis: f -- F = { (f - w) where w is Element of ExtREAL : w in F }
thus f -- F c= { (f - w) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def 10 :: thesis: { (f - w) 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 { (f - w) where w is Element of ExtREAL : w in F } )
assume e in f -- F ; :: thesis: e in { (f - w) where w is Element of ExtREAL : w in F }
then consider w1, w2 being Element of ExtREAL such that
A1: e = w1 + w2 and
A2: ( w1 in {f} & w2 in -- F ) ;
A3: w1 - (- w2) = w1 + w2 ;
( - w2 in F & w1 = f ) by A2, Th2, TARSKI:def 1;
hence e in { (f - w) where w is Element of ExtREAL : w in F } by A1, A3; :: thesis: verum

end;

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