let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; :: thesis: 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; :: thesis: ex p being POINT of S st reflection (a,p) = p9
set p = reflection (a,p9);
take reflection (a,p9) ; :: thesis: reflection (a,(reflection (a,p9))) = p9
thus reflection (a,(reflection (a,p9))) = p9 by Satz7p7; :: thesis: verum