theorem :: EUCLID_8:54
for p being Element of REAL 3 holds len (- p) = len p