theorem LmISRank41: :: ZMODUL06:57

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st rank (W1 /\ W2) = rank W1 holds
for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V