theorem :: CLVECT_1:59

for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2