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 x1, p2 being Point of (TOP-REAL n) such that
A1: ( p = x1 + p2 & x1 in X & p2 in Y (+) Z ) ;
consider y, z being Point of (TOP-REAL n) such that
A2: ( p2 = y + z & y in Y & z in Z ) by A1;
A3: p = (x1 + y) + z by A1, A2, EUCLID:30;
set p3 = x1 + y;
x1 + y in X (+) Y by A1, A2;
hence p in (X (+) Y) (+) Z by A2, A3; :: 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 x1, p2 being Point of (TOP-REAL n) such that
A4: ( p = x1 + p2 & x1 in X (+) Y & p2 in Z ) ;
consider y, z being Point of (TOP-REAL n) such that
A5: ( x1 = y + z & y in X & z in Y ) by A4;
A6: p = y + (z + p2) by A4, A5, EUCLID:30;
set p3 = z + p2;
z + p2 in Y (+) Z by A4, A5;
hence p in X (+) (Y (+) Z) by A5, A6; :: thesis: verum