let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( between a,c,b & a,b <= a,c implies b = c )
assume A1: ( between a,c,b & a,b <= a,c ) ; :: thesis: 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; :: thesis: verum