theorem :: GTARSKI3:15

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b being POINT of S holds between a,a,b by Satz3p1, Satz3p2;