for V being RealLinearSpace
for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)