theorem Satz4p5: :: GTARSKI3:43

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, a9, c9 being POINT of S st between a,b,c & a,c equiv a9,c9 holds
ex b9 being POINT of S st
( between a9,b9,c9 & a,b,c cong a9,b9,c9 )