for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S st p out a,b & p out b,c holds
p out a,c by Satz3p6p2, Satz5p3, Satz5p1;