theorem LmRankSX2: :: ZMODUL07:7

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Submodule of V
for I1 being Basis of W1 ex I being finite linearly-independent Subset of V st
( I is Subset of (W1 + W2) & I1 c= I & rank (W1 + W2) = rank (Lin I) )