theorem Th16: :: EUCLID_2:18

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