let a, b be POINT of TarskiEuclid2Space; :: thesis: ( a = b iff dist (a,b) = 0 )

hereby :: thesis: ( dist (a,b) = 0 implies a = b )

assume a = b ; :: thesis: dist (a,b) = 0
then Tn2R a = Tn2R b ;
then 0 = |.((Tn2TR a) - (Tn2TR b)).| ;
hence dist (a,b) = 0 by ThEquiv; :: thesis: verum

end;

assume dist (a,b) = 0 ; :: thesis: a = b
hence a = b by METRIC_1:2; :: thesis: verum