theorem :: EUCLID_5:11
for x1, y1, z1 being Real holds - |[x1,y1,z1]| = |[(- x1),(- y1),(- z1)]|