theorem :: GTARSKI3:133

for S being (IE) (SC) TarskiGeometryStruct
for a, b being POINT of S holds between a,b,b by Satz3p1;