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