let A, B be POINT of TarskiEuclid2Space; :: thesis: ( dist (A,B) = |.((Tn2TR A) - (Tn2TR B)).| & dist (A,B) = |.((Tn2R A) - (Tn2R B)).| )
MetrStruct(# the U1 of TarskiEuclid2Space, the distance of TarskiEuclid2Space #) = MetrStruct(# the U1 of (Euclid 2), the distance of (Euclid 2) #) by GTARSKI1:def 13;
then dist (A,B) = (Pitag_dist 2) . ((Tn2TR A),(Tn2TR B)) by METRIC_1:def 1
.= |.((Tn2R A) - (Tn2R B)).| by EUCLID:def 6 ;
hence ( dist (A,B) = |.((Tn2TR A) - (Tn2TR B)).| & dist (A,B) = |.((Tn2R A) - (Tn2R B)).| ) ; :: thesis: verum