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 set ; :: 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 ;
A4: e = w1 - (- w2) by A1;
- w2 in G by A3, Th8;
hence e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by A4, A2; :: thesis: verum

end;

let e be set ; :: 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
A5: e = w1 - w2 and
A6: w1 in F and
A7: w2 in G ;
- w2 in -- G by A7;
hence e in F -- G by A5, A6; :: thesis: verum