theorem EqDist2PointsBetween: :: GTARSKI1:35
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p, q being POINT of S st a <> b & between a,b,c & a,p equiv a,q & b,p equiv b,q holds
c,p equiv c,q