theorem :: ZMODUL01:131

for V being Z_Module
for W1, W2 being Submodule of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2 by VECTSP_5:45;