for L being Z_Lattice
for L1 being Z_Sublattice of L
for v being Vector of L st v in L1 holds
- v in L1