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