for AFV being WeakAffVect
for a, b, c, b9, c9 being Element of AFV st Mid a,b,c & Mid a,b9,c9 & MDist b,b9 holds
c = c9