theorem :: GTARSKI3:134

for S being (TE) (SC) TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b equiv c,d holds
c,d equiv a,b by Satz2p2bis;