let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; for a, p9 being POINT of S ex p being POINT of S st reflection (a,p) = p9
let a, p9 be POINT of S; ex p being POINT of S st reflection (a,p) = p9
set p = reflection (a,p9);
take
reflection (a,p9)
; reflection (a,(reflection (a,p9))) = p9
thus
reflection (a,(reflection (a,p9))) = p9
by Satz7p7; verum