let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( between p,q,r implies between reflection (a,p), reflection (a,q), reflection (a,r) )
assume A1: between p,q,r ; :: thesis: 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; :: thesis: verum