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,c equiv a9,c9 & b,c equiv b9,c9 holds
a,b equiv a9,b9
let a, b, c, a9, b9, c9 be POINT of S; :: thesis: ( between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 implies a,b equiv a9,b9 )
assume A1: ( between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 ) ; :: thesis: a,b equiv a9,b9
then c,a equiv a9,c9 by Satz2p4;
then a,b,c,a IFS a9,b9,c9,a9 by A1, Satz2p8, Satz2p5;
then a,b equiv b9,a9 by Satz4p2, Satz2p4;
hence a,b equiv a9,b9 by Satz2p5; :: thesis: verum