theorem :: EUCLID_8:62

for p1, p2 being Element of REAL 3 holds p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]|