theorem ThConv3: :: GTARSKI2:17

for A, B being POINT of TarskiEuclid2Space holds
( dist (A,B) = |.((Tn2TR A) - (Tn2TR B)).| & dist (A,B) = |.((Tn2R A) - (Tn2R B)).| )