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,c,d
let a, b, c, d be POINT of S; :: thesis: ( between a,b,c & between b,c,d & b <> c implies between a,c,d )
assume A1: ( between a,b,c & between b,c,d & b <> c ) ; :: thesis: between a,c,d
consider x being POINT of S such that
A2: ( between a,c,x & c,x equiv c,d ) by GTARSKI1:def 8;
A3: between b,c,x by A1, A2, Satz3p6p1;
c,d equiv c,d by Satz2p1;
hence between a,c,d by A1, A2, A3, Satz2p12; :: thesis: verum