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