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

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

suppose a = b ; :: thesis: b,c equiv b9,c9

hence b,c equiv b9,c9 by H4, A3, EquivSymmetric, H3; :: thesis: verum

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;

end;