let L be INTegral Z_Lattice; :: thesis: GramDet L is Integer
set b = the OrdBasis of L;
GramMatrix the OrdBasis of L is Matrix of dim L,INT.Ring by ThIntLatY;
then Det (GramMatrix the OrdBasis of L) in INT by ZMATRLIN:47;
hence GramDet L is Integer by defGramDet; :: thesis: verum