let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

between a,b,c

let a, b, c, d be POINT of S; :: thesis: ( between a,b,d & between b,c,d implies between a,b,c )

assume H1: between a,b,d ; :: thesis: ( not between b,c,d or between a,b,c )

assume between b,c,d ; :: thesis: between a,b,c

then consider x being POINT of S such that

X1: ( between b,x,b & between c,x,a ) by H1, A7;

b = x by X1, A6;

hence between a,b,c by Bsymmetry, X1; :: thesis: verum

between a,b,c

let a, b, c, d be POINT of S; :: thesis: ( between a,b,d & between b,c,d implies between a,b,c )

assume H1: between a,b,d ; :: thesis: ( not between b,c,d or between a,b,c )

assume between b,c,d ; :: thesis: between a,b,c

then consider x being POINT of S such that

X1: ( between b,x,b & between c,x,a ) by H1, A7;

b = x by X1, A6;

hence between a,b,c by Bsymmetry, X1; :: thesis: verum