theorem Th19: :: EUCLID_2:21

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds |((- p1),p2)| = - |(p1,p2)|