:: deftheorem defines out GTARSKI3:def 8 :
for S being TarskiGeometryStruct
for a, b, p being POINT of S holds
( p out a,b iff ( p <> a & p <> b & ( between p,a,b or between p,b,a ) ) );