:: deftheorem defZLattice defines Z_Lattice-like ZMODLAT1:def 3 :
for IT being non empty LatticeStr over INT.Ring holds
( IT is Z_Lattice-like iff ( ( for x being Vector of IT st ( for y being Vector of IT holds <;x,y;> = 0 ) holds
x = 0. IT ) & ( for x, y being Vector of IT holds <;x,y;> = <;y,x;> ) & ( for x, y, z being Vector of IT
for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) ) ) );