theorem :: ZMODLAT1:28

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