let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, p being POINT of S st reflection (a,p) = reflection (b,p) holds
a = b
let a, b, p be POINT of S; :: thesis: ( reflection (a,p) = reflection (b,p) implies a = b )
assume A1: reflection (a,p) = reflection (b,p) ; :: thesis: a = b
( Middle p,a, reflection (a,p) & Middle p,b, reflection (b,p) ) by DEFR;
hence a = b by A1, Satz7p17; :: thesis: verum