theorem :: ZMODUL07:10

for V being free finite-rank Z_Module
for W1, W2 being Submodule of V holds rank (W1 /\ W2) >= ((rank W1) + (rank W2)) - (rank V)