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 b,c,d holds
between b,d,c
let a, b, c, d be POINT of S; :: thesis: ( a <> b & between a,b,c & between a,b,d & not between b,c,d implies between b,d,c )
assume A1: ( a <> b & between a,b,c & between a,b,d ) ; :: thesis: ( between b,c,d or between b,d,c )
then ( between a,c,d or between a,d,c ) by Satz5p1;
hence ( between b,c,d or between b,d,c ) by A1, Satz3p6p1; :: thesis: verum