theorem :: GTARSKI3:75

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S st p out a,b holds
p out b,a ;