for S being (TE) (SC) (FS') TarskiGeometryStruct
for a, b, c, d, e, f being POINT of S st a <> b & between b,a,c & between d,a,e & b,a equiv d,a & a,c equiv a,e & b,f equiv d,f holds
f,c equiv e,f