let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( a <> b & between a,b,c & between a,b,d & not between b,d,c implies between b,c,d )
assume H1:
a <> b
; ( 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
; ( 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 H4:
(
b <> c &
b <> d &
c <> d )
;
( between b,d,c or between b,c,d )assume H5:
not
between b,
d,
c
;
between b,c,dconsider 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
;
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;
verum
end; hence
between b,
c,
d
by X3, Z4, EquivSymmetric, A3;
verum end; end;