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