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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (+) {(0.REAL n)} or x in X )
assume x in X (+) {(0.REAL n)} ; :: thesis: x in X
then consider y, z being Point of (TOP-REAL n) such that
A1: ( x = y + z & y in X & z in {(0.REAL n)} ) ;
{z} c= {(0.REAL n)} by A1, ZFMISC_1:37;
then z = 0.REAL n by ZFMISC_1:24;
hence x in X by A1, EUCLID:31; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X (+) {(0.REAL n)} )
assume A2: x in X ; :: thesis: x in X (+) {(0.REAL n)}
then reconsider x = x as Point of (TOP-REAL n) ;
0.REAL n in {(0.REAL n)} by TARSKI:def 1;
then x + (0.REAL n) in { (y + z) where y, z is Point of (TOP-REAL n) : ( y in X & z in {(0.REAL n)} ) } by A2;
hence x in X (+) {(0.REAL n)} by EUCLID:31; :: thesis: verum