theorem :: ZMODUL06:71

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Submodule of V st rank (W1 /\ W2) = rank W1 holds
ex a being Element of INT.Ring st a (*) W1 is Submodule of W2