let F, G be ext-real-membered set ; :: thesis: for f being ExtReal holds (f ++ F) \ (f ++ G) c= f ++ (F \ G)
let f be ExtReal; :: thesis: (f ++ F) \ (f ++ G) c= f ++ (F \ G)
let i be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not i in (f ++ F) \ (f ++ G) or i in f ++ (F \ G) )
assume A1: i in (f ++ F) \ (f ++ G) ; :: thesis: i in f ++ (F \ G)
then consider w being Element of ExtREAL such that
A2: i = f + w and
A3: w in F by Th134;
now :: thesis: w in F \ G
assume not w in F \ G ; :: thesis: contradiction
then w in G by A3, XBOOLE_0:def 5;
then f + w in f ++ G by Th132;
hence contradiction by A1, A2, XBOOLE_0:def 5; :: thesis: verum
end;
hence i in f ++ (F \ G) by A2, Th132; :: thesis: verum