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 A1: B = the carrier of E ; :: thesis: B (-) A = B

hence B = B (-) A by A1; :: thesis: verum

B (-) A = B

let A, B be Subset of E; :: thesis: ( B = the carrier of E implies B (-) A = B )

assume A1: B = the carrier of E ; :: thesis: B (-) A = B

now :: thesis: for x being object st x in the carrier of E holds

x in B (-) A

then
the carrier of E c= B (-) A
;x in B (-) A

let x be object ; :: 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 A1;

hence x in B (-) A ; :: thesis: verum

end;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 A1;

hence x in B (-) A ; :: thesis: verum

hence B = B (-) A by A1; :: thesis: verum