theorem Th12: :: GTARSKI5:12

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, c, r being POINT of S
for A being Subset of S st between a,A,c & r in A holds
for b being POINT of S st r out a,b holds
between b,A,c