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 H2, X1, B123and134Ordered;

then X3: between u,c,b by Bsymmetry;

u,c equiv c,u by A1;

then X4: u,c equiv b,d by X1, EquivTransitive;

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 H3, Y1, B123and134Ordered;

Y4: b,c equiv d,x by Y1, EquivSymmetric;

c,b equiv b,c by A1;

then c,b equiv d,x by Y4, EquivTransitive;

then X6: u,b equiv b,x by X3, Y2, X4, SegmentAddition;

b,u equiv u,b by A1;

then u = x by H1, X2, Y2, C1, X6, EquivTransitive;

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

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 H2, X1, B123and134Ordered;

then X3: between u,c,b by Bsymmetry;

u,c equiv c,u by A1;

then X4: u,c equiv b,d by X1, EquivTransitive;

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 H3, Y1, B123and134Ordered;

Y4: b,c equiv d,x by Y1, EquivSymmetric;

c,b equiv b,c by A1;

then c,b equiv d,x by Y4, EquivTransitive;

then X6: u,b equiv b,x by X3, Y2, X4, SegmentAddition;

b,u equiv u,b by A1;

then u = x by H1, X2, Y2, C1, X6, EquivTransitive;

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