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