let E be RealLinearSpace; :: thesis: for A, B being Subset of E st B = the carrier of E & A <> {} holds
( A (+) B = B & B (+) A = B )
let A, B be Subset of E; :: thesis: ( B = the carrier of E & A <> {} implies ( A (+) B = B & B (+) A = B ) )
assume AS: ( B = the carrier of E & A <> {} ) ; :: thesis: ( A (+) B = B & B (+) A = B )
then consider a being set such that
P1: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of E by P1;

now :: thesis: for x being set st x in the carrier of E holds
x in A (+) B

let x be set ; :: thesis: ( x in the carrier of E implies x in A (+) B )
assume x in the carrier of E ; :: thesis: x in A (+) B
then reconsider z = x as Element of E ;
a + (z - a) = z by RLVECT_4:1;
hence x in A (+) B by AS, P1; :: thesis: verum

end;

then P1: the carrier of E c= A (+) B by TARSKI:def 3;
hence B = A (+) B by AS, XBOOLE_0:def 10; :: thesis: B (+) A = B
thus B (+) A = A + B
.= B by P1, AS, XBOOLE_0:def 10 ; :: thesis: verum