theorem ThSLX2: :: ZMODLAT2:26

for L being positive-definite Z_Lattice
for Z being non empty LatticeStr over INT.Ring st Z is Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z holds
Z is Z_Lattice-like