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