for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, m being POINT of S st Collinear a,m,b & m,a equiv m,b & not a = b holds
Middle a,m,b