let F, G be ext-real-membered set ; :: thesis: -- (F \ G) = (-- F) \ (-- G)
let i be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not i in -- (F \ G) or i in (-- F) \ (-- G) ) & ( not i in (-- F) \ (-- G) or i in -- (F \ G) ) )

hereby :: thesis: ( not i in (-- F) \ (-- G) or i in -- (F \ G) )

assume i in -- (F \ G) ; :: thesis: i in (-- F) \ (-- G)
then A1: - i in F \ G by Th2;
then not - i in G by XBOOLE_0:def 5;
then A2: not i in -- G by Th2;
i in -- F by A1, Th2;
hence i in (-- F) \ (-- G) by A2, XBOOLE_0:def 5; :: thesis: verum

end;

assume A3: i in (-- F) \ (-- G) ; :: thesis: i in -- (F \ G)
then not i in -- G by XBOOLE_0:def 5;
then A4: not - i in G by Th2;
- i in F by A3, Th2;
then - i in F \ G by A4, XBOOLE_0:def 5;
hence i in -- (F \ G) by Th2; :: thesis: verum