let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y being Subset of T holds X (+) Y = Y (+) X
let X, Y be Subset of T; :: 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 object ; :: 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 ex p1, p2 being Point of T st
( p = p1 + p2 & p1 in X & p2 in Y ) ;
hence p in Y (+) X ; :: thesis: verum

end;

let p be object ; :: 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 ex p1, p2 being Point of T st
( p = p1 + p2 & p1 in Y & p2 in X ) ;
hence p in X (+) Y ; :: thesis: verum