let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, x, a9, b9, c9, x9 being POINT of S st a,b,c cong a9,b9,c9 & between a,x,c & between a9,x9,c9 & c,x equiv c9,x9 holds
b,x equiv b9,x9
let a, b, c, x, a9, b9, c9, x9 be POINT of S; :: thesis: ( a,b,c cong a9,b9,c9 & between a,x,c & between a9,x9,c9 & c,x equiv c9,x9 implies b,x equiv b9,x9 )
assume that
H1: a,b,c cong a9,b9,c9 and
H2: between a,x,c and
H3: between a9,x9,c9 and
H4: c,x equiv c9,x9 ; :: thesis: b,x equiv b9,x9
X1: ( a,b equiv a9,b9 & a,c equiv a9,c9 & b,c equiv b9,c9 ) by H1;

per cases ( x = c or x <> c ) ;

suppose x = c ; :: thesis: b,x equiv b9,x9

hence b,x equiv b9,x9 by H1, A3, H4, EquivSymmetric; :: thesis: verum

end;

suppose x <> c ; :: thesis: b,x equiv b9,x9

then X2: a <> c by H2, A6;
consider y being POINT of S such that
X3: ( between a,c,y & c,y equiv a,c ) by A4;
consider y9 being POINT of S such that
X4: ( between a9,c9,y9 & c9,y9 equiv a,c ) by A4;
a,c equiv c9,y9 by X4, EquivSymmetric;
then X5: c,y equiv c9,y9 by X3, EquivTransitive;
X6: c,b equiv c9,b9 by H1, CongruenceDoubleSymmetry;
then a,c,b cong a9,c9,b9 by X1;
then X7: b,y equiv b9,y9 by X2, X3, X4, X5, A5;
X8: y <> c by X3, EquivSymmetric, A3, X2;
( between y,c,a & between c,x,a ) by X3, H2, Bsymmetry;
then X9: between y,c,x by B124and234then123;
( between y9,c9,a9 & between c9,x9,a9 ) by X4, H3, Bsymmetry;
then X10: between y9,c9,x9 by B124and234then123;
y,c,b cong y9,c9,b9 by X6, X5, X7, CongruenceDoubleSymmetry;
hence b,x equiv b9,x9 by X8, X9, X10, H4, A5; :: thesis: verum

end;

end;