theorem Th29: :: EUCLID_5:29

for p1, p2 being Point of (TOP-REAL 3) holds |(p1,p2)| = (((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))