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

proof

A4: c,a equiv a,b by A1, Satz2p4;
a,b equiv a,c by A1, Satz2p2;
then b,a equiv a,c by Satz2p4;
hence c,b,a cong b,c,a by A4, Satz2p5, GTARSKI1:def 5; :: thesis: verum

end;

between b,c,a by A2, A3, Satz4p6;
hence c = b by A2, Satz3p4; :: thesis: verum