let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for c, d, e, d9 being POINT of S st between d,e,d9 & c,d9 equiv c,d & d,e equiv d9,e & c <> d & e <> d holds
ex p, r, q being POINT of S st
( between p,r,q & between r,c,d9 & between e,c,p & r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e )

let c, d, e, d9 be POINT of S; :: thesis: ( between d,e,d9 & c,d9 equiv c,d & d,e equiv d9,e & c <> d & e <> d implies ex p, r, q being POINT of S st
( between p,r,q & between r,c,d9 & between e,c,p & r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e ) )

assume that
H2: between d,e,d9 and
H3: c,d9 equiv c,d and
H4: d,e equiv d9,e and
H5: c <> d and
H6: e <> d ; :: thesis: ex p, r, q being POINT of S st
( between p,r,q & between r,c,d9 & between e,c,p & r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e )

c <> d9 by ;
then consider p, r being POINT of S such that
X1: ( between e,c,p & between d9,c,r & p,r,c cong d9,e,c ) by EasyAngleTransport;
d9,e equiv d,e by ;
then X3: p,r equiv d,e by ;
then X4: p <> r by ;
consider q being POINT of S such that
X5: ( between p,r,q & r,q equiv e,d ) by A4;
X6: between d9,e,d by ;
c,p equiv c,d9 by ;
then X7: c,p equiv c,d by ;
c,q equiv c,d by X4, X1, X5, X6, A5;
then c,d equiv c,q by EquivSymmetric;
then X8: c,p equiv c,q by ;
X10: r,p equiv e,d by ;
e,d equiv r,q by ;
then X11: r,c,p cong r,c,q by ;
between r,c,d9 by ;
hence ex p, r, q being POINT of S st
( between p,r,q & between r,c,d9 & between e,c,p & r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e ) by X5, X11, X1, X3; :: thesis: verum