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

proof

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

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} or a in {(0. (TOP-REAL n))} + x )
assume a in {x} ; :: thesis: a in {(0. (TOP-REAL n))} + x
then {a} c= {x} by ZFMISC_1:37;
then a = x by ZFMISC_1:24;
then A3: a = (0. (TOP-REAL n)) + x by EUCLID:31;
0. (TOP-REAL n) in {(0. (TOP-REAL n))} by ZFMISC_1:37;
hence a in {(0. (TOP-REAL n))} + x by A3; :: thesis: verum