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;

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 )
;

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;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