theorem :: ZMODLAT1:25

for L being Z_Lattice
for L1, L2 being Z_Sublattice of L holds 0. L1 = 0. L2