theorem A7: :: GTARSKI1:9

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds
ex x being POINT of S st
( between p,x,b & between q,x,a )