let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d holds
ex x being POINT of S st
( a,b,c,x are_ordered & a,b,d,x are_ordered )

let a, b, c, d be POINT of S; :: thesis: ( a <> b & between a,b,c & between a,b,d implies ex x being POINT of S st
( a,b,c,x are_ordered & a,b,d,x are_ordered ) )

assume that
H1: a <> b and
H2: between a,b,c and
H3: between a,b,d ; :: thesis: ex x being POINT of S st
( a,b,c,x are_ordered & a,b,d,x are_ordered )

consider u being POINT of S such that
X1: ( between a,c,u & c,u equiv b,d ) by A4;
X2: a,b,c,u are_ordered by ;
then X3: between u,c,b by Bsymmetry;
u,c equiv c,u by A1;
then X4: u,c equiv b,d by ;
consider x being POINT of S such that
Y1: ( between a,d,x & d,x equiv b,c ) by A4;
Y2: a,b,d,x are_ordered by ;
Y4: b,c equiv d,x by ;
c,b equiv b,c by A1;
then c,b equiv d,x by ;
then X6: u,b equiv b,x by ;
b,u equiv u,b by A1;
then u = x by ;
hence ex x being POINT of S st
( a,b,c,x are_ordered & a,b,d,x are_ordered ) by X2, Y2; :: thesis: verum