theorem ThSL1: :: ZMODLAT1:21

for L being Z_Lattice
for L1 being Z_Sublattice of L holds L1 is Submodule of L