let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a being POINT of S holds reflection (a,a) = a
let a be POINT of S; :: thesis: reflection (a,a) = a
Middle a,a,a by GTARSKI3:97;
hence reflection (a,a) = a by GTARSKI3:100; :: thesis: verum