let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, c, p, q, x being POINT of S st between a,x,c & a,p equiv a,q & c,p equiv c,q holds

x,p equiv x,q

let a, c, p, q, x be POINT of S; :: thesis: ( between a,x,c & a,p equiv a,q & c,p equiv c,q implies x,p equiv x,q )

assume H1: between a,x,c ; :: thesis: ( not a,p equiv a,q or not c,p equiv c,q or x,p equiv x,q )

assume H2: ( a,p equiv a,q & c,p equiv c,q ) ; :: thesis: x,p equiv x,q

X1: ( a,c equiv a,c & c,x equiv c,x ) by EquivReflexive;

then a,p,c cong a,q,c by H2, CongruenceDoubleSymmetry;

then p,x equiv q,x by H1, X1, Inner5Segments;

hence x,p equiv x,q by CongruenceDoubleSymmetry; :: thesis: verum

x,p equiv x,q

let a, c, p, q, x be POINT of S; :: thesis: ( between a,x,c & a,p equiv a,q & c,p equiv c,q implies x,p equiv x,q )

assume H1: between a,x,c ; :: thesis: ( not a,p equiv a,q or not c,p equiv c,q or x,p equiv x,q )

assume H2: ( a,p equiv a,q & c,p equiv c,q ) ; :: thesis: x,p equiv x,q

X1: ( a,c equiv a,c & c,x equiv c,x ) by EquivReflexive;

then a,p,c cong a,q,c by H2, CongruenceDoubleSymmetry;

then p,x equiv q,x by H1, X1, Inner5Segments;

hence x,p equiv x,q by CongruenceDoubleSymmetry; :: thesis: verum