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