let p, q, r, s be Point of TarskiEuclid2Space; :: thesis: ( q <> r & between p,q,r & between q,r,s implies between p,q,s )
assume that
A1: q <> r and
A2: between p,q,r and
A3: between q,r,s ; :: thesis: between p,q,s
A4: Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r)) by A2, ThConv6;
then A5: (dist ((Tn2TR p),(Tn2TR q))) + (dist ((Tn2TR q),(Tn2TR r))) = dist ((Tn2TR p),(Tn2TR r)) by EUCLID12:12;
A6: Tn2TR r in LSeg ((Tn2TR q),(Tn2TR s)) by A3, ThConv6;
A7: Tn2TR r in LSeg ((Tn2TR p),(Tn2TR s)) by A1, A4, A6, THORANGE2;
(dist ((Tn2TR p),(Tn2TR q))) + (dist ((Tn2TR q),(Tn2TR s))) = ((dist ((Tn2TR p),(Tn2TR r))) - (dist ((Tn2TR q),(Tn2TR r)))) + ((dist ((Tn2TR q),(Tn2TR r))) + (dist ((Tn2TR r),(Tn2TR s)))) by A5, A6, EUCLID12:12
.= (dist ((Tn2TR p),(Tn2TR r))) + (dist ((Tn2TR r),(Tn2TR s)))
.= dist ((Tn2TR p),(Tn2TR s)) by A7, EUCLID12:12 ;
then Tn2TR q in LSeg ((Tn2TR p),(Tn2TR s)) by EUCLID12:12;
hence between p,q,s by ThConv6; :: thesis: verum