for S being (TE) (SC) TarskiGeometryStruct
for a, b being POINT of S holds a,b equiv a,b by Satz2p1bis;