theorem :: ZMODLAT1:34

for L being Z_Lattice
for L1 being Z_Sublattice of L
for v being Vector of L
for a being Element of INT.Ring st v in L1 holds
a * v in L1