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

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