theorem ThISRank4: :: ZMODUL06:59
for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V st rank (W1 /\ W2) = rank W1 holds
rank (W1 + W2) = rank W2