let p, q be POINT of TarskiEuclid2Space; :: thesis: dist (p,q) = sqrt (((((Tn2TR p) `1) - ((Tn2TR q) `1)) ^2) + ((((Tn2TR p) `2) - ((Tn2TR q) `2)) ^2))
A1: MetrStruct(# the U1 of TarskiEuclid2Space, the distance of TarskiEuclid2Space #) = MetrStruct(# the U1 of (Euclid 2), the distance of (Euclid 2) #) by GTARSKI1:def 13;
(Pitag_dist 2) . ((Tn2E p),(Tn2E q)) = sqrt (((((Tn2TR p) `1) - ((Tn2TR q) `1)) ^2) + ((((Tn2TR p) `2) - ((Tn2TR q) `2)) ^2)) by TOPREAL3:7;
hence dist (p,q) = sqrt (((((Tn2TR p) `1) - ((Tn2TR q) `1)) ^2) + ((((Tn2TR p) `2) - ((Tn2TR q) `2)) ^2)) by A1, METRIC_1:def 1; :: thesis: verum