let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; :: thesis: for a, p, p9 being POINT of S st reflection (a,p) = reflection (a,p9) holds
p = p9
let a, p, p9 be POINT of S; :: thesis: ( reflection (a,p) = reflection (a,p9) implies p = p9 )
assume reflection (a,p) = reflection (a,p9) ; :: thesis: p = p9
then reflection (a,(reflection (a,p))) = p9 by Satz7p7;
hence p = p9 by Satz7p7; :: thesis: verum