let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, c9 being POINT of S st between a,c,b & a,c equiv a,c9 & b,c equiv b,c9 holds
c = c9
let a, b, c, c9 be POINT of S; :: thesis: ( between a,c,b & a,c equiv a,c9 & b,c equiv b,c9 implies c = c9 )
assume A1: ( between a,c,b & a,c equiv a,c9 & b,c equiv b,c9 ) ; :: thesis: c = c9
A2: ( a = b implies c = c9 )

proof

assume a = b ; :: thesis: c = c9
then a = c by A1, GTARSKI1:def 10;
hence c = c9 by A1, Satz2p2, GTARSKI1:def 7; :: thesis: verum

end;

( a <> b implies c = c9 )

proof

assume A3: a <> b ; :: thesis: c = c9
Collinear a,b,c by A1, Satz3p2;
hence c = c9 by A1, A3, Satz4p18; :: thesis: verum

end;

hence c = c9 by A2; :: thesis: verum