theorem Lem01: :: GTARSKI4:14

for S being satisfying_Tarski-model TarskiGeometryStruct
for a being POINT of S holds reflection (a,a) = a