theorem :: ZMODLAT1:32

for L being Z_Lattice
for L1 being Z_Sublattice of L holds 0. L1 in L