let p, q, r, s be Point of TarskiEuclid2Space; :: thesis: ( between p,q,r & between p,s,q implies between s,q,r )
assume that
A1: between p,q,r and
A2: between p,s,q ; :: thesis: between s,q,r
A3: Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r)) by A1, ThConv6;
Tn2TR s in LSeg ((Tn2TR p),(Tn2TR q)) by A2, ThConv6;
then Tn2TR q in LSeg ((Tn2TR s),(Tn2TR r)) by A3, THNOIX;
hence between s,q,r by ThConv6; :: thesis: verum