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