theorem Satz3p11p3pb: :: GTARSKI3:26
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S st between a,b,c & between b,p,c holds
between4 a,b,p,c by Satz3p5p1, Satz3p5p2;