for L being Z_Lattice
for b being OrdBasis of L st GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat holds
L is RATional