for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st c,a equiv c,b holds
ex x being POINT of S st Middle a,x,b