let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, d, p being POINT of S st between4 a,b,c,d & between b,p,c holds
between5 a,b,p,c,d
let a, b, c, d, p be POINT of S; ( between4 a,b,c,d & between b,p,c implies between5 a,b,p,c,d )
assume A1:
( between4 a,b,c,d & between b,p,c )
; between5 a,b,p,c,d
then
( between a,b,p & between p,c,d & between b,p,c & between b,p,d & between a,p,c )
by Satz3p5p1, Satz3p5p2, Satz3p6p1, Satz3p6p2;
hence
between5 a,b,p,c,d
by A1, Satz3p5p2; verum