let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S holds a,a <= b,c
let a, b, c be POINT of S; :: thesis: a,a <= b,c
ex x being POINT of S st
( between a,a,x & a,x equiv b,c ) by GTARSKI1:def 8;
hence a,a <= b,c by Satz5p5; :: thesis: verum