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 H5, H3, EquivSymmetric, A3;
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 H4, EquivSymmetric;
then X3: p,r equiv d,e by X1, EquivTransitive;
then X4: p <> r by EquivSymmetric, H6, A3;
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 H2, Bsymmetry;
c,p equiv c,d9 by X1, CongruenceDoubleSymmetry;
then X7: c,p equiv c,d by H3, EquivTransitive;
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 X7, EquivTransitive;
X10: r,p equiv e,d by X3, CongruenceDoubleSymmetry;
e,d equiv r,q by X5, EquivSymmetric;
then X11: r,c,p cong r,c,q by EquivReflexive, X8, X10, EquivTransitive;
between r,c,d9 by X1, Bsymmetry;
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