let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, d being POINT of S st between a,b,d & between a,c,d & not between a,b,c holds
between a,c,b
let a, b, c, d be POINT of S; ( between a,b,d & between a,c,d & not between a,b,c implies between a,c,b )
assume A1:
( between a,b,d & between a,c,d )
; ( between a,b,c or between a,c,b )
per cases
( a = b or a <> b )
;
suppose A2:
a <> b
;
( between a,b,c or between a,c,b )consider p being
POINT of
S such that A3:
(
between d,
a,
p &
a,
p equiv a,
b )
by GTARSKI1:def 8;
A4:
a <> p
by A3, Satz2p2, A2, GTARSKI1:def 7;
between p,
a,
d
by A3, Satz3p2;
then
(
between p,
a,
b &
between p,
a,
c )
by A1, Satz3p5p1;
hence
(
between a,
b,
c or
between a,
c,
b )
by A4, Satz5p2;
verum end; end;