let n be Element of NAT ; :: thesis: for X, Y, Z being Subset of (TOP-REAL n) holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z
let X, Y, Z be Subset of (TOP-REAL n); :: thesis: X (+) (Y (-) Z) c= (X (+) Y) (-) Z
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (+) (Y (-) Z) or x in (X (+) Y) (-) Z )
assume x in X (+) (Y (-) Z) ; :: thesis: x in (X (+) Y) (-) Z
then consider a, b being Point of (TOP-REAL n) such that
A1: x = a + b and
A2: a in X and
A3: b in Y (-) Z ;
ex c being Point of (TOP-REAL n) st
( b = c & Z + c c= Y ) by A3;
then (Z + b) + a c= Y + a by Th3;
then A4: Z + (b + a) c= Y + a by Th16;
Y + a c= Y (+) X by A2, Th19;
then Z + (b + a) c= Y (+) X by A4, XBOOLE_1:1;
then x in (Y (+) X) (-) Z by A1;
hence x in (X (+) Y) (-) Z by Th12; :: thesis: verum