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 H1, H2, Bsymmetry;

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 H3, EquivSymmetric;

X4: c,c9 equiv c,c9 by EquivReflexive;

c,d equiv d9,c9 by H5, EquivSymmetric;

then c,d,c9 cong c,d9,c9 by X3, X4, H4, EquivTransitive;

then X5: d,e equiv d9,e by X2, EquivReflexive, Inner5Segments;

X6: d,c equiv c,d by A1;

c,d equiv d,c9 by H4, EquivSymmetric;

then X7: d,c equiv d,c9 by X6, EquivTransitive;

X9: c,d equiv d9,c9 by H5, EquivSymmetric;

d9,c9 equiv c9,d9 by A1;

then c,d equiv c9,d9 by X9, EquivTransitive;

then c,d9 equiv c9,d9 by H3, EquivTransitive;

then d,c,d9 cong d,c9,d9 by X7, EquivReflexive;

then c,e equiv c9,e by X2, EquivReflexive, Inner5Segments;

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

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 H1, H2, Bsymmetry;

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 H3, EquivSymmetric;

X4: c,c9 equiv c,c9 by EquivReflexive;

c,d equiv d9,c9 by H5, EquivSymmetric;

then c,d,c9 cong c,d9,c9 by X3, X4, H4, EquivTransitive;

then X5: d,e equiv d9,e by X2, EquivReflexive, Inner5Segments;

X6: d,c equiv c,d by A1;

c,d equiv d,c9 by H4, EquivSymmetric;

then X7: d,c equiv d,c9 by X6, EquivTransitive;

X9: c,d equiv d9,c9 by H5, EquivSymmetric;

d9,c9 equiv c9,d9 by A1;

then c,d equiv c9,d9 by X9, EquivTransitive;

then c,d9 equiv c9,d9 by H3, EquivTransitive;

then d,c,d9 cong d,c9,d9 by X7, EquivReflexive;

then c,e equiv c9,e by X2, EquivReflexive, Inner5Segments;

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