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