:: deftheorem defIntegral defines INTegral ZMODLAT1:def 5 :
for IT being Z_Lattice holds
( IT is INTegral iff for v, u being Vector of IT holds <;v,u;> in INT );