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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (+) {(0. (TOP-REAL n))} or x in X )
assume x in X (+) {(0. (TOP-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 ) and
A2: z in {(0. (TOP-REAL n))} ;
{z} c= {(0. (TOP-REAL n))} by A2, ZFMISC_1:37;
then z = 0. (TOP-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. (TOP-REAL n))} )
assume A3: x in X ; :: thesis: x in X (+) {(0. (TOP-REAL n))}
then reconsider x = x as Point of (TOP-REAL n) ;
0. (TOP-REAL n) in {(0. (TOP-REAL n))} by TARSKI:def 1;
then x + (0. (TOP-REAL n)) in { (y + z) where y, z is Point of (TOP-REAL n) : ( y in X & z in {(0. (TOP-REAL n))} ) } by A3;
hence x in X (+) {(0. (TOP-REAL n))} by EUCLID:31; :: thesis: verum