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