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

proof

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

end;

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