let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b being POINT of S st ( Middle a,a,b or Middle a,b,b or Middle a,b,a ) holds
a = b
let a, b be POINT of S; :: thesis: ( ( Middle a,a,b or Middle a,b,b or Middle a,b,a ) implies a = b )
assume ( Middle a,a,b or Middle a,b,b or Middle a,b,a ) ; :: thesis: a = b
then ( a,a equiv a,b or b,a equiv b,b or Middle a,b,a ) by GTARSKI3:def 12;
hence a = b by GTARSKI1:def 7, GTARSKI3:3, GTARSKI3:97; :: thesis: verum