theorem :: EUCLID_8:54

for p being Element of REAL 3 holds len (- p) = len p