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 & a in X & b in Y (-) Z ) ;
consider c being Point of (TOP-REAL n) such that
A2: ( b = c & Z + c c= Y ) by A1;
(Z + b) + a c= Y + a by A2, Th3;
then A3: Z + (b + a) c= Y + a by Th16;
Y + a c= Y (+) X by A1, Th19;
then Z + (b + a) c= Y (+) X by A3, XBOOLE_1:1;
then x in (Y (+) X) (-) Z by A1;
hence x in (X (+) Y) (-) Z by Th12; :: thesis: verum