theorem ThGM2: :: ZMODLAT2:70

for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of L holds Det (GramMatrix b) <> 0. F_Real