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