let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( 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
; 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
;
b,x equiv b9,x9then 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;
verum end;