:: deftheorem defines ||. ZMODLAT1:def 2 :
for X being non empty LatticeStr over INT.Ring
for x being Vector of X holds ||.x.|| = <;x,x;>;