let F, G be ext-real-membered set ; :: thesis: F -- G = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }
thus F -- G c= { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } :: according to XBOOLE_0:def 10 :: thesis: { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } c= F -- G

proof

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

end;

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