let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c being POINT of S st between a,c,b & a,b <= a,c holds
b = c
let a, b, c be POINT of S; ( between a,c,b & a,b <= a,c implies b = c )
assume A1:
( between a,c,b & a,b <= a,c )
; b = c
then consider x being POINT of S such that
A2:
( between a,b,x & a,x equiv a,c )
by Satz5p5;
c = x
by A1, A2, Lemma5p12p3, Satz3p6p2;
hence
b = c
by A1, A2, Satz3p6p1, GTARSKI1:def 10; verum