theorem Th26: :: EUCLID_2:28

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