let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d, e being POINT of S st b <> c & c <> d & between b,c,d & ( between a,b,c or between b,a,c ) & ( between c,d,e or between c,e,d ) holds
between a,c,e
let a, b, c, d, e be POINT of S; :: thesis: ( b <> c & c <> d & between b,c,d & ( between a,b,c or between b,a,c ) & ( between c,d,e or between c,e,d ) implies between a,c,e )
assume that
A1: b <> c and
A2: c <> d and
A3: between b,c,d and
A4: ( between a,b,c or between b,a,c ) and
A5: ( between c,d,e or between c,e,d ) ; :: thesis: between a,c,e
between a,c,d by A1, A3, A4, GTARSKI3:18, GTARSKI3:19;
hence between a,c,e by A2, A5, GTARSKI3:17, GTARSKI3:19; :: thesis: verum