theorem A5: :: GTARSKI1:7

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, x, a9, b9, c9, x9 being POINT of S st a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 holds
c,x equiv c9,x9