let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & a,c equiv a9,c9 holds
b,c equiv b9,c9
let a, b, c, a9, b9, c9 be POINT of S; ( between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & a,c equiv a9,c9 implies b,c equiv b9,c9 )
assume that
H1:
between a,b,c
and
H2:
between a9,b9,c9
and
H3:
a,b equiv a9,b9
and
H4:
a,c equiv a9,c9
; b,c equiv b9,c9
per cases
( a = b or a <> b )
;
suppose Z1:
a <> b
;
b,c equiv b9,c9consider x being
POINT of
S such that Z2:
(
between a,
b,
x &
b,
x equiv b9,
c9 )
by A4;
Z3:
a,
x equiv a9,
c9
by Z2, H2, H3, SegmentAddition;
a9,
c9 equiv a,
c
by H4, EquivSymmetric;
then
a,
x equiv a,
c
by Z3, EquivTransitive;
hence
b,
c equiv b9,
c9
by Z1, Z2, H1, C1prime;
verum end;