theorem ThRankS5: :: ZMODUL06:69

for V being torsion-free Z_Module
for W1, W2, W3 being free finite-rank Submodule of V st rank (W1 + W2) = rank W2 & W3 is Submodule of W1 holds
rank (W3 + W2) = rank W2