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 )

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 ) )
;

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

end;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

hence
between b,c,d
by X3, Z4, EquivSymmetric, A3; :: thesis: verum
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;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