theorem :: EUCLID:60

for x1, y1 being Real holds - |[x1,y1]| = |[(- x1),(- y1)]|