theorem Satz2p8: :: GTARSKI3:8

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct
for a, b being POINT of S holds a,a equiv b,b