theorem :: GTARSKI5:3

for S being non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st between a,A,b holds
between b,A,a by GTARSKI3:14;