theorem :: ZMODLAT3:45

for L being Z_Lattice
for b being OrdBasis of L st GramMatrix ((InnerProduct L),b) is Matrix of dim L,INT.Ring holds
L is INTegral