theorem Satz2p1bis: :: GTARSKI3:2

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