let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st between a,b,d & between a,c,d & not between a,b,c holds
between a,c,b
let a, b, c, d be POINT of S; :: thesis: ( between a,b,d & between a,c,d & not between a,b,c implies between a,c,b )
assume A1: ( between a,b,d & between a,c,d ) ; :: thesis: ( between a,b,c or between a,c,b )
per cases ( a = b or a <> b ) ;
suppose a = b ; :: thesis: ( between a,b,c or between a,c,b )
hence ( between a,b,c or between a,c,b ) by Satz3p1, Satz3p2; :: thesis: verum
end;
suppose A2: a <> b ; :: thesis: ( between a,b,c or between a,c,b )
consider p being POINT of S such that
A3: ( between d,a,p & a,p equiv a,b ) by GTARSKI1:def 8;
A4: a <> p by A3, Satz2p2, A2, GTARSKI1:def 7;
between p,a,d by A3, Satz3p2;
then ( between p,a,b & between p,a,c ) by A1, Satz3p5p1;
hence ( between a,b,c or between a,c,b ) by A4, Satz5p2; :: thesis: verum
end;
end;