let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: b,c equiv b9,c9

b,c equiv b9,c9

let a, b, c, a9, b9, c9 be POINT of S; :: thesis: ( 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 ; :: thesis: b,c equiv b9,c9

per cases
( a = b or a <> b )
;

end;

suppose Z1:
a <> b
; :: thesis: b,c equiv b9,c9

consider 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; :: thesis: verum

end;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; :: thesis: verum