let E be RealLinearSpace; :: thesis: for A, B being Subset of E st B = the carrier of E holds
B (-) A = B
let A, B be Subset of E; :: thesis: ( B = the carrier of E implies B (-) A = B )
assume AS: B = the carrier of E ; :: thesis: B (-) A = B

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

let x be set ; :: thesis: ( x in the carrier of E implies x in B (-) A )
assume x in the carrier of E ; :: thesis: x in B (-) A
then reconsider z = x as Element of E ;
for a being Element of E st a in A holds
z - a in B by AS;
hence x in B (-) A ; :: thesis: verum

end;

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