let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, p, q, r, s being POINT of S st p,q equiv r,s holds
reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s)
let a, p, q, r, s be POINT of S; ( p,q equiv r,s implies reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) )
assume A1:
p,q equiv r,s
; reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s)
A2:
r,s equiv reflection (a,r), reflection (a,s)
by Satz7p13;
p,q equiv reflection (a,p), reflection (a,q)
by Satz7p13;
then
r,s equiv reflection (a,p), reflection (a,q)
by A1, GTARSKI1:def 6;
hence
reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s)
by A2, GTARSKI1:def 6; verum