theorem ThConv2: :: GTARSKI2:16

for p, q being POINT of TarskiEuclid2Space holds dist (p,q) = sqrt (((((Tn2TR p) `1) - ((Tn2TR q) `1)) ^2) + ((((Tn2TR p) `2) - ((Tn2TR q) `2)) ^2))