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;
per cases ( a = b or a <> b ) ;
suppose a = b ; :: thesis: a,c equiv a9,c9
hence a,c equiv a9,c9 by H3, H4, A3, EquivSymmetric; :: thesis: verum
end;
suppose Z1: a <> b ; :: thesis: a,c equiv a9,c9
a9,b9 equiv b9,a9 by A1;
then b,a equiv b9,a9 by Z2, EquivTransitive;
then a,b,a cong a9,b9,a9 by H3, Baaa;
hence a,c equiv a9,c9 by Z1, H1, H2, H4, A5; :: thesis: verum
end;
end;