let p, q, r be POINT of TarskiEuclid2Space; ( p is_Between q,r iff Tn2TR p in LSeg ((Tn2TR q),(Tn2TR r)) )
A1:
( dist ((Tn2TR q),(Tn2TR p)) = dist ((Tn2E q),(Tn2E p)) & dist ((Tn2TR p),(Tn2TR r)) = dist ((Tn2E p),(Tn2E r)) & dist ((Tn2TR q),(Tn2TR r)) = dist ((Tn2E q),(Tn2E r)) )
by TOPREAL6:def 1;
( dist (q,p) = dist ((Tn2E q),(Tn2E p)) & dist (p,r) = dist ((Tn2E p),(Tn2E r)) & dist (q,r) = dist ((Tn2E q),(Tn2E r)) )
by ThConv;
hence
( p is_Between q,r iff Tn2TR p in LSeg ((Tn2TR q),(Tn2TR r)) )
by A1, EUCLID12:12; verum