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 & b,c equiv b9,c9 holds

a,c equiv a9,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 & b,c equiv b9,c9 implies a,c equiv a9,c9 )

assume that

H1: between a,b,c and

H2: between a9,b9,c9 and

H3: a,b equiv a9,b9 and

H4: b,c equiv b9,c9 ; :: thesis: a,c equiv a9,c9

b,a equiv a,b by A1;

then Z2: b,a equiv a9,b9 by H3, EquivTransitive;

a,c equiv a9,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 & b,c equiv b9,c9 implies a,c equiv a9,c9 )

assume that

H1: between a,b,c and

H2: between a9,b9,c9 and

H3: a,b equiv a9,b9 and

H4: b,c equiv b9,c9 ; :: thesis: a,c equiv a9,c9

b,a equiv a,b by A1;

then Z2: b,a equiv a9,b9 by H3, EquivTransitive;