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 q being Point of (TOP-REAL n) such that
A1: ( x = q + (0. (TOP-REAL n)) & q in X ) ;
thus 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 A2: x in X ; :: thesis: x in X + (0. (TOP-REAL n))
then reconsider x1 = x as Point of (TOP-REAL n) ;
x1 = x1 + (0. (TOP-REAL n)) by EUCLID:31;
hence x in X + (0. (TOP-REAL n)) by A2; :: thesis: verum