for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, a1, b1, c1 being Element of S st b out a,c & b1 out a1,c1 & b,a equiv b1,a1 & b,c equiv b1,c1 holds
a,c equiv a1,c1