theorem :: ZMODLAT1:17

for L being positive-definite Z_Lattice
for v being Vector of L holds ||.v.|| >= 0