let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, p being POINT of S holds
( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b )
let a, b, p be POINT of S; :: thesis: ( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b )
( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) implies a = b )

proof

assume A1: reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) ; :: thesis: a = b
set p9 = reflection (a,p);
A2: Middle p,a, reflection (a,p) by DEFR;
Middle reflection (b,p),a, reflection (b,(reflection (a,p))) by A1, DEFR;
then Middle reflection (b,(reflection (b,p))), reflection (b,a), reflection (b,(reflection (b,(reflection (a,p))))) by Satz7p15, Satz7p16;
then Middle p, reflection (b,a), reflection (b,(reflection (b,(reflection (a,p))))) by Satz7p7;
then Middle p, reflection (b,a), reflection (a,p) by Satz7p7;
hence a = b by A2, Satz7p17, Satz7p10; :: thesis: verum

end;

hence ( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b ) ; :: thesis: verum