theorem :: CLVECT_1:37
for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds 0. W1 in W2