theorem :: GTARSKI5:2

for S being non empty satisfying_BetweennessIdentity TarskiGeometryStruct
for a being POINT of S
for A being Subset of S holds not between a,A,a by GTARSKI1:def 10;