let n be Element of NAT ; :: thesis: for X, Y being Subset of (TOP-REAL n) holds X (+) Y = Y (+) X
let X, Y be Subset 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 p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in X (+) Y or p in Y (+) X )
assume p in X (+) Y ; :: thesis: p in Y (+) X
then consider p1, p2 being Point of (TOP-REAL n) such that
A1: ( p = p1 + p2 & p1 in X & p2 in Y ) ;
thus p in Y (+) X by A1; :: thesis: verum

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in Y (+) X or p in X (+) Y )
assume p in Y (+) X ; :: thesis: p in X (+) Y
then consider p1, p2 being Point of (TOP-REAL n) such that
A2: ( p = p1 + p2 & p1 in Y & p2 in X ) ;
thus p in X (+) Y by A2; :: thesis: verum