let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st b <> c & between a,b,c & between b,c,d holds
between a,c,d
let a, b, c, d be POINT of S; :: thesis: ( b <> c & between a,b,c & between b,c,d implies between a,c,d )
assume that
H1: b <> c and
H2: between a,b,c and
H3: between b,c,d ; :: thesis: between a,c,d
consider x being POINT of S such that
X1: ( between a,c,x & c,x equiv c,d ) by A4;
X2: between x,c,a by X1, Bsymmetry;
between c,b,a by H2, Bsymmetry;
then between x,c,b by X2, B124and234then123;
then between b,c,x by Bsymmetry;
hence between a,c,d by X1, H1, H3, C1; :: thesis: verum