let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum