let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, d, p being POINT of S st between4 a,b,c,d & between c,d,p holds
( between c,d,p & ( c <> d implies between5 a,b,c,d,p ) )
let a, b, c, d, p be POINT of S; ( between4 a,b,c,d & between c,d,p implies ( between c,d,p & ( c <> d implies between5 a,b,c,d,p ) ) )
assume A1:
( between4 a,b,c,d & between c,d,p )
; ( between c,d,p & ( c <> d implies between5 a,b,c,d,p ) )
hence
between c,d,p
; ( c <> d implies between5 a,b,c,d,p )
hereby verum
assume
c <> d
;
between5 a,b,c,d,pthen
(
between b,
c,
p &
between b,
d,
p &
between a,
c,
p &
between a,
d,
p )
by A1, Satz3p7p1, Satz3p7p2;
hence
between5 a,
b,
c,
d,
p
by A1, Satz3p7p2;
verum
end;