let n be Element of NAT ; :: thesis: for X, Y, Z being Subset of (TOP-REAL n) holds X (-) (Y (+) Z) = (X (-) Y) (-) Z
let X, Y, Z be Subset of (TOP-REAL n); :: thesis: X (-) (Y (+) Z) = (X (-) Y) (-) Z
thus X (-) (Y (+) Z) c= (X (-) Y) (-) Z :: according to XBOOLE_0:def 10 :: thesis: (X (-) Y) (-) Z c= X (-) (Y (+) Z)

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in X (-) (Y (+) Z) or p in (X (-) Y) (-) Z )
assume p in X (-) (Y (+) Z) ; :: thesis: p in (X (-) Y) (-) Z
then consider x being Point of (TOP-REAL n) such that
A1: ( p = x & (Y (+) Z) + x c= X ) ;
(Y + x) (+) Z c= X by A1, Th15;
then Z (+) (Y + x) c= X by Th12;
then A2: (Z (+) (Y + x)) (-) (Y + x) c= X (-) (Y + x) by Th9;
Z c= (Z (+) (Y + x)) (-) (Y + x) by Th20;
then Z c= X (-) (Y + x) by A2, XBOOLE_1:1;
then Z c= (X (-) Y) + (- x) by Th17;
then Z + x c= ((X (-) Y) + (- x)) + x by Th3;
then Z + x c= (X (-) Y) + ((- x) + x) by Th16;
then Z + x c= (X (-) Y) + (x - x) by EUCLID:45;
then Z + x c= (X (-) Y) + (0. (TOP-REAL n)) by EUCLID:46;
then Z + x c= X (-) Y by Th21;
hence p in (X (-) Y) (-) Z by A1; :: thesis: verum

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in (X (-) Y) (-) Z or p in X (-) (Y (+) Z) )
assume p in (X (-) Y) (-) Z ; :: thesis: p in X (-) (Y (+) Z)
then consider y being Point of (TOP-REAL n) such that
A3: ( p = y & Z + y c= X (-) Y ) ;
A4: (Z + y) (+) Y c= (X (-) Y) (+) Y by A3, Th9;
(X (-) Y) (+) Y c= X by Lm2;
then (Z + y) (+) Y c= X by A4, XBOOLE_1:1;
then (Z (+) Y) + y c= X by Th15;
then p in X (-) (Z (+) Y) by A3;
hence p in X (-) (Y (+) Z) by Th12; :: thesis: verum