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