for V being RealLinearSpace
for W1, W2 being Subspace of V holds 0. W1 in W2