let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, p, q, r being POINT of S st between p,q,r holds
between reflection (a,p), reflection (a,q), reflection (a,r)
let a, p, q, r be POINT of S; ( between p,q,r implies between reflection (a,p), reflection (a,q), reflection (a,r) )
assume A1:
between p,q,r
; between reflection (a,p), reflection (a,q), reflection (a,r)
p,q,r cong reflection (a,p), reflection (a,q), reflection (a,r)
by Satz7p13;
hence
between reflection (a,p), reflection (a,q), reflection (a,r)
by A1, Satz4p6; verum