theorem :: ZMODUL06:68

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Submodule of V
for v being VECTOR of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V holds
W2 /\ (Lin {v}) <> (0). V