theorem ThRatLat1B: :: ZMODLAT3:46

for L being Z_Lattice
for I being finite Subset of L
for u being Vector of L st ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in RAT