let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, p, q being POINT of S st a <> b & between a,b,c & a,p equiv a,q & b,p equiv b,q holds
c,p equiv c,q
let a, b, c, p, q be POINT of S; :: thesis: ( a <> b & between a,b,c & a,p equiv a,q & b,p equiv b,q implies c,p equiv c,q )
assume H1: a <> b ; :: thesis: ( not between a,b,c or not a,p equiv a,q or not b,p equiv b,q or c,p equiv c,q )
assume H2: between a,b,c ; :: thesis: ( not a,p equiv a,q or not b,p equiv b,q or c,p equiv c,q )
assume H3: ( a,p equiv a,q & b,p equiv b,q ) ; :: thesis: c,p equiv c,q
a,b,p cong a,b,q by H3, EquivReflexive;
then p,c equiv q,c by H1, H2, EquivReflexive, A5;
hence c,p equiv c,q by CongruenceDoubleSymmetry; :: thesis: verum