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 b,d,p holds
( between4 b,c,d,p & ( b <> d implies between5 a,b,c,d,p ) )
let a, b, c, d, p be POINT of S; :: thesis: ( between4 a,b,c,d & between b,d,p implies ( between4 b,c,d,p & ( b <> d implies between5 a,b,c,d,p ) ) )
assume A1: ( between4 a,b,c,d & between b,d,p ) ; :: thesis: ( between4 b,c,d,p & ( b <> d implies between5 a,b,c,d,p ) )
hence between4 b,c,d,p by Satz3p6p1, Satz3p6p2; :: thesis: ( b <> d implies between5 a,b,c,d,p )
thus ( b <> d implies between5 a,b,c,d,p ) :: thesis: verum

proof

assume b <> d ; :: thesis: between5 a,b,c,d,p
then ( between a,b,p & between a,d,p ) by A1, Satz3p7p1, Satz3p7p2;
hence between5 a,b,c,d,p by A1, Satz3p6p1, Satz3p6p2; :: thesis: verum

end;