:: deftheorem defines <; ZMODLAT1:def 1 :
for X being non empty LatticeStr over INT.Ring
for x, y being Vector of X holds <;x,y;> = the scalar of X . [x,y];