theorem Th51: :: EUCLID_8:60

for p being Element of REAL 3 holds - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]|