let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; 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; ( reflection (a,p) = reflection (a,p9) implies p = p9 )
assume
reflection (a,p) = reflection (a,p9)
; p = p9
then
reflection (a,(reflection (a,p))) = p9
by Satz7p7;
hence
p = p9
by Satz7p7; verum