for L being RATional Z_Lattice
for LX being Z_Lattice st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
LX is RATional