let a, b be Point of TarskiEuclid2Space; :: thesis: ( between a,b,a implies a = b )
assume between a,b,a ; :: thesis: a = b
then Tn2TR b in LSeg ((Tn2TR a),(Tn2TR a)) by ThConv6;
then Tn2TR b in {(Tn2TR a)} by RLTOPSP1:70;
hence a = b by TARSKI:def 1; :: thesis: verum