theorem Th52: :: EUCLID_8:61

for p being Element of REAL 3 holds
( (- p) . 1 = - (p . 1) & (- p) . 2 = - (p . 2) & (- p) . 3 = - (p . 3) )