theorem :: VECTSP_9:33

for GF being Field
for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)