let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( 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
; 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; verum