theorem :: ZMODUL06:56

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Submodule of V
for I being Basis of W1 st rank (W1 /\ W2) < rank W1 holds
ex v being VECTOR of V st
( v in I & (W1 /\ W2) /\ (Lin {v}) = (0). V ) by ThISRank2;