theorem :: ZMODLAT2:57

for L being RATional Z_Lattice
for b being OrdBasis of L holds Det (GramMatrix b) in F_Rat