for V being RealLinearSpace
for W1, W2 being Subspace of V
for v being VECTOR of V st ( v in W1 or v in W2 ) holds
v in W1 + W2