let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; :: thesis: for a, p being POINT of S holds reflection (a,(reflection (a,p))) = p
let a, p be POINT of S; :: thesis: reflection (a,(reflection (a,p))) = p
Middle p,a, reflection (a,p) by DEFR;
then Middle reflection (a,p),a,p by Satz3p2, Satz2p2;
hence reflection (a,(reflection (a,p))) = p by DEFR; :: thesis: verum