let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( between a,b,c & a,c equiv a,b implies c = b )
assume A1:
( between a,b,c & a,c equiv a,b )
; 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;
verum
end;
between b,c,a
by A2, A3, Satz4p6;
hence
c = b
by A2, Satz3p4; verum