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