theorem Th12: :: EUCLID_5:12

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