let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for b, c, d, c9, d9 being POINT of S st between b,c,d9 & between b,d,c9 & c,d9 equiv c,d & d,c9 equiv c,d & d9,c9 equiv c,d holds
ex e being POINT of S st
( between c,e,c9 & between d,e,d9 & c,e equiv c9,e & d,e equiv d9,e )

let b, c, d, c9, d9 be POINT of S; :: thesis: ( between b,c,d9 & between b,d,c9 & c,d9 equiv c,d & d,c9 equiv c,d & d9,c9 equiv c,d implies ex e being POINT of S st
( between c,e,c9 & between d,e,d9 & c,e equiv c9,e & d,e equiv d9,e ) )

assume that
H1: between b,c,d9 and
H2: between b,d,c9 and
H3: c,d9 equiv c,d and
H4: d,c9 equiv c,d and
H5: d9,c9 equiv c,d ; :: thesis: ex e being POINT of S st
( between c,e,c9 & between d,e,d9 & c,e equiv c9,e & d,e equiv d9,e )

( between d9,c,b & between c9,d,b ) by ;
then consider e being POINT of S such that
X2: ( between c,e,c9 & between d,e,d9 ) by A7;
X3: c,d equiv c,d9 by ;
X4: c,c9 equiv c,c9 by EquivReflexive;
c,d equiv d9,c9 by ;
then c,d,c9 cong c,d9,c9 by ;
then X5: d,e equiv d9,e by ;
X6: d,c equiv c,d by A1;
c,d equiv d,c9 by ;
then X7: d,c equiv d,c9 by ;
X9: c,d equiv d9,c9 by ;
d9,c9 equiv c9,d9 by A1;
then c,d equiv c9,d9 by ;
then c,d9 equiv c9,d9 by ;
then d,c,d9 cong d,c9,d9 by ;
then c,e equiv c9,e by ;
hence ex e being POINT of S st
( between c,e,c9 & between d,e,d9 & c,e equiv c9,e & d,e equiv d9,e ) by X2, X5; :: thesis: verum