for a, b, c, d being POINT of TarskiEuclid2Space holds
( (dist (a,b)) ^2 = (dist (c,d)) ^2 iff a,b equiv c,d )