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 & not between b,d,c holds
between b,c,d

let a, b, c, d be POINT of S; :: thesis: ( a <> b & between a,b,c & between a,b,d & not between b,d,c implies between b,c,d )
assume H1: a <> b ; :: thesis: ( not between a,b,c or not between a,b,d or between b,d,c or between b,c,d )
assume that
H2: between a,b,c and
H3: between a,b,d ; :: thesis: ( between b,d,c or between b,c,d )
per cases ( b = c or b = d or c = d or ( b <> c & b <> d & c <> d ) ) ;
suppose ( b = c or b = d or c = d ) ; :: thesis: ( between b,d,c or between b,c,d )
hence ( between b,d,c or between b,c,d ) by ; :: thesis: verum
end;
suppose H4: ( b <> c & b <> d & c <> d ) ; :: thesis: ( between b,d,c or between b,c,d )
assume H5: not between b,d,c ; :: thesis: between b,c,d
consider d9 being POINT of S such that
X1: ( between a,c,d9 & c,d9 equiv c,d ) by A4;
consider c9 being POINT of S such that
X2: ( between a,d,c9 & d,c9 equiv c,d ) by A4;
x3: a,b,c,d9 are_ordered by ;
then X3: ( between a,b,d9 & between b,c,d9 ) ;
x4: a,b,d,c9 are_ordered by ;
X5: c <> d9 by ;
X6: d <> c9 by ;
X7: b <> d9 by x3, H4, A6;
X8: b <> c9 by x4, H4, A6;
consider u being POINT of S such that
Y1: ( between c,d9,u & d9,u equiv b,d ) by A4;
y2: b,c,d9,u are_ordered by ;
consider b9 being POINT of S such that
Y3: ( between d,c9,b9 & c9,b9 equiv b,c ) by A4;
y4: b,d,c9,b9 are_ordered by ;
Y5: between c9,d,b by ;
Y6: ( d,c9 equiv c9,d & b,d equiv d,b ) by A1;
c,d equiv d,c9 by ;
then c,d9 equiv d,c9 by ;
then Y7: c,d9 equiv c9,d by ;
d9,u equiv d,b by ;
then Y8: c,u equiv c9,b by ;
Y9: ( c9,b9 equiv b9,c9 & b9,b equiv b,b9 ) by A1;
b,c equiv c9,b9 by ;
then Y10: b,c equiv b9,c9 by ;
between b9,c9,b by ;
then b,u equiv b9,b by ;
then Y11: b,u equiv b,b9 by ;
Y12: a,b,d9,u are_ordered by ;
a,b,c9,b9 are_ordered by ;
then Y13: u = b9 by H1, Y11, C1, Y12;
c9,b equiv c,b9 by ;
then b,c9 equiv b9,c by CongruenceDoubleSymmetry;
then Z2: b,c,c9 cong b9,c9,c by ;
between b9,c9,d by ;
then Z3: c9,d9 equiv c,d by H4, Z2, X3, Y7, A5;
d9,c9 equiv c9,d9 by A1;
then d9,c9 equiv c,d by ;
then consider e being POINT of S such that
Z4: ( between c,e,c9 & between d,e,d9 & c,e equiv c9,e & d,e equiv d9,e ) by ;
U1: e <> c by ;
e = d
proof
assume V2: e <> d ; :: thesis: contradiction
then consider p, r, q being POINT of S such that
W1: ( between p,r,q & between r,c,d9 & between e,c,p & r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e ) by ;
c <> r by ;
then W3: d9,p equiv d9,q by ;
then W4: b9,p equiv b9,q by ;
between d9,c,b by ;
then W5: b,p equiv b,q by ;
W7: c9,p equiv c9,q by ;
between c9,e,c by ;
then w8: c9,e,c,p are_ordered by ;
c9 <> c by Z4, U1, A6;
then p,p equiv p,q by ;
then q = p by ;
then p = r by W1, A6;
hence contradiction by V2, W1, EquivSymmetric, A3; :: thesis: verum
end;
hence between b,c,d by ; :: thesis: verum
end;
end;