theorem Satz6p3: :: GTARSKI3:72

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S holds
( p out a,b iff ( a <> p & b <> p & ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c ) ) )