:: deftheorem defRational defines RATional ZMODLAT2:def 1 :
for IT being Z_Lattice holds
( IT is RATional iff for v, u being Vector of IT holds <;v,u;> in RAT );