let p, q, r be POINT of TarskiEuclid2Space; :: thesis: ( 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; :: thesis: verum