let a, b, c be Point of TarskiEuclid2Space; :: thesis: ( between a,b,c implies between c,b,a )
assume between a,b,c ; :: thesis: between c,b,a
then Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c)) by ThConv6;
hence between c,b,a by ThConv6; :: thesis: verum