let p, q, r, s be Point of TarskiEuclid2Space; ( 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
; 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; verum