for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d IFS a9,b9,c9,d9 holds
b,d equiv b9,d9