:: deftheorem defines are_orthogonal ZMODLAT1:def 8 :
for L being Z_Lattice
for v, u being Vector of L holds
( v,u are_orthogonal iff <;v,u;> = 0 );