theorem ThIS1: :: ZMODUL06:3

for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 /\ W2 <> (0). V holds
(W1 + W3) /\ W2 <> (0). V