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 Baaq, Bqaa; :: 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 H2, X1, B123and134Ordered;
then X3: ( between a,b,d9 & between b,c,d9 ) ;
x4: a,b,d,c9 are_ordered by H3, X2, B123and134Ordered;
X5: c <> d9 by X1, H4, A3, EquivSymmetric;
X6: d <> c9 by X2, H4, A3, EquivSymmetric;
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 X5, x3, Y1, BTransitivityOrdered;
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 X6, x4, Y3, BTransitivityOrdered;
Y5: between c9,d,b by x4, Bsymmetry;
Y6: ( d,c9 equiv c9,d & b,d equiv d,b ) by A1;
c,d equiv d,c9 by X2, EquivSymmetric;
then c,d9 equiv d,c9 by X1, EquivTransitive;
then Y7: c,d9 equiv c9,d by Y6, EquivTransitive;
d9,u equiv d,b by Y1, Y6, EquivTransitive;
then Y8: c,u equiv c9,b by Y1, Y5, Y7, SegmentAddition;
Y9: ( c9,b9 equiv b9,c9 & b9,b equiv b,b9 ) by A1;
b,c equiv c9,b9 by Y3, EquivSymmetric;
then Y10: b,c equiv b9,c9 by Y9, EquivTransitive;
between b9,c9,b by y4, Bsymmetry;
then b,u equiv b9,b by y2, Y10, Y8, SegmentAddition;
then Y11: b,u equiv b,b9 by Y9, EquivTransitive;
Y12: a,b,d9,u are_ordered by X7, x3, y2, BTransitivityOrdered;
a,b,c9,b9 are_ordered by X8, x4, y4, BTransitivityOrdered;
then Y13: u = b9 by H1, Y11, C1, Y12;
c9,b equiv c,b9 by Y13, Y8, EquivSymmetric;
then b,c9 equiv b9,c by CongruenceDoubleSymmetry;
then Z2: b,c,c9 cong b9,c9,c by Y10, A1;
between b9,c9,d by Y3, Bsymmetry;
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 Z3, EquivTransitive;
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 X1, X2, RhombusDiagBisect;
U1: e <> c by H5, x4, Z4, EquivSymmetric, A3;
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 Z4, X1, H4, FlatNormal;
c <> r by W1, U1, EquivSymmetric, A3;
then W3: d9,p equiv d9,q by W1, EqDist2PointsBetween;
then W4: b9,p equiv b9,q by X5, W1, Y1, Y13, EqDist2PointsBetween;
between d9,c,b by X3, Bsymmetry;
then W5: b,p equiv b,q by X5, W3, W1, EqDist2PointsBetween;
W7: c9,p equiv c9,q by y4, W4, W5, EqDist2PointsInnerBetween;
between c9,e,c by Z4, Bsymmetry;
then w8: c9,e,c,p are_ordered by U1, W1, BTransitivityOrdered;
c9 <> c by Z4, U1, A6;
then p,p equiv p,q by w8, W7, W1, EqDist2PointsBetween;
then q = p by EquivSymmetric, A3;
then p = r by W1, A6;
hence contradiction by V2, W1, EquivSymmetric, A3; :: thesis: verum
end;
hence between b,c,d by X3, Z4, EquivSymmetric, A3; :: thesis: verum
end;
end;