theorem Th35: :: RLVECT_5:35

for V being finite-dimensional RealLinearSpace
for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)