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

proof

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

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in X + x or p in X (+) {x} )
assume p in X + x ; :: thesis: p in X (+) {x}
then consider q being Point of (TOP-REAL n) such that
A2: ( p = q + x & q in X ) ;
x in {x} by TARSKI:def 1;
hence p in X (+) {x} by A2; :: thesis: verum