theorem LmISRank51X: :: ZMODUL06:62

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V holds (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)