for AFV being WeakAffSegm
for a, b, c, p, p9 being Element of AFV st a,b // p,p9 & a,b // b,c & a,p // p,b & a,p9 // p9,b holds
a = c