let F, G be ext-real-membered set ; :: thesis: for r being Real holds r ++ (F \ G) = (r ++ F) \ (r ++ G)
let r be Real; :: thesis: r ++ (F \ G) = (r ++ F) \ (r ++ G)
A1: r ++ (F \ G) c= (r ++ F) \ (r ++ G)

proof

let i be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not i in r ++ (F \ G) or i in (r ++ F) \ (r ++ G) )
assume i in r ++ (F \ G) ; :: thesis: i in (r ++ F) \ (r ++ G)
then consider w being Element of ExtREAL such that
A2: i = r + w and
A3: w in F \ G by Th134;

A4: now :: thesis: not r + w in r ++ G

assume r + w in r ++ G ; :: thesis: contradiction
then consider w1 being Element of ExtREAL such that
A5: r + w = r + w1 and
A6: w1 in G by Th134;
w = w1 by A5, XXREAL_3:11;
hence contradiction by A3, A6, XBOOLE_0:def 5; :: thesis: verum

end;

r + w in r ++ F by A3, Th132;
hence i in (r ++ F) \ (r ++ G) by A2, A4, XBOOLE_0:def 5; :: thesis: verum

end;

(r ++ F) \ (r ++ G) c= r ++ (F \ G) by Th138;
hence r ++ (F \ G) = (r ++ F) \ (r ++ G) by A1; :: thesis: verum