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