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

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