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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (+) (Y + p) or x in (X (+) Y) + p )
assume x in X (+) (Y + p) ; :: thesis: x in (X (+) Y) + p
then consider x2, y2 being Point of (TOP-REAL n) such that
A1: ( x = x2 + y2 & x2 in X & y2 in Y + p ) ;
consider y3 being Point of (TOP-REAL n) such that
A2: ( y2 = y3 + p & y3 in Y ) by A1;
A3: x = (x2 + y3) + p by A1, A2, EUCLID:30;
x2 + y3 in X (+) Y by A1, A2;
hence x in (X (+) Y) + p by A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (+) Y) + p or x in X (+) (Y + p) )
assume x in (X (+) Y) + p ; :: thesis: x in X (+) (Y + p)
then consider x2 being Point of (TOP-REAL n) such that
A4: ( x = x2 + p & x2 in X (+) Y ) ;
consider x3, y3 being Point of (TOP-REAL n) such that
A5: ( x2 = x3 + y3 & x3 in X & y3 in Y ) by A4;
A6: x = x3 + (y3 + p) by A4, A5, EUCLID:30;
y3 + p in Y + p by A5;
hence x in X (+) (Y + p) by A5, A6; :: thesis: verum