theorem :: EUCLID_4:24

for n being Nat
for x1, x2 being Element of REAL n holds |(x1,(- x2))| = - |(x1,x2)| by Th23;