let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct ; :: thesis: for a, p being POINT of S holds
( reflection (a,p) = p iff p = a )
let a, p be POINT of S; :: thesis: ( reflection (a,p) = p iff p = a )
hereby :: thesis: ( p = a implies reflection (a,p) = p )
assume reflection (a,p) = p ; :: thesis: p = a
then Middle p,a,p by DEFR;
hence p = a by GTARSKI1:def 10; :: thesis: verum
end;
assume p = a ; :: thesis: reflection (a,p) = p
then Middle p,a,p by Satz3p1, Satz2p1;
hence reflection (a,p) = p by DEFR; :: thesis: verum