theorem EqDist2PointsInnerBetween: :: GTARSKI1:36

for S being satisfying_Tarski-model TarskiPlane
for a, c, p, q, x being POINT of S st between a,x,c & a,p equiv a,q & c,p equiv c,q holds
x,p equiv x,q