theorem ThSc1: :: ZMODLAT1:7
for L being Z_Lattice
for v, u being Vector of L holds
( <;v,(- u);> = - <;v,u;> & <;(- v),u;> = - <;v,u;> )