theorem ThSL4: :: ZMODLAT1:24

for L being Z_Lattice
for L1 being Z_Sublattice of L
for w being Vector of L1 holds w is Vector of L