let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds
between a,c,d
let a, b, c, d be POINT of S; :: thesis: ( between a,b,d & between b,c,d implies between a,c,d )
assume A1: ( between a,b,d & between b,c,d ) ; :: thesis: between a,c,d
then between a,b,c by Satz3p5p1;
hence between a,c,d by A1, Satz3p7p1; :: thesis: verum