theorem Satz2p1: :: GTARSKI3:1

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct
for a, b being POINT of S holds a,b equiv a,b