let a, b, c be POINT of TarskiEuclid2Space; :: according to GTARSKI1:def 7 :: thesis: ( not a,b equiv c,c or a = b )
assume a,b equiv c,c ; :: thesis: a = b
then dist (a,b) = dist (c,c) by GTARSKI1:def 15;
hence a = b by METRIC_1:2, METRIC_1:1; :: thesis: verum