let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( 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 )
; 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; verum