let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, p, q, r being POINT of S holds
( between p,q,r iff between reflection (a,p), reflection (a,q), reflection (a,r) )
let a, p, q, r be POINT of S; :: thesis: ( between p,q,r iff between reflection (a,p), reflection (a,q), reflection (a,r) )
now :: thesis: ( between reflection (a,p), reflection (a,q), reflection (a,r) implies between p,q,r )
assume C1: between reflection (a,p), reflection (a,q), reflection (a,r) ; :: thesis: between p,q,r
( reflection (a,(reflection (a,p))) = p & reflection (a,(reflection (a,q))) = q & reflection (a,(reflection (a,r))) = r ) by Satz7p7;
hence between p,q,r by C1, Lemma7p15a; :: thesis: verum
end;
hence ( between p,q,r iff between reflection (a,p), reflection (a,q), reflection (a,r) ) by Lemma7p15a; :: thesis: verum