theorem :: AFVECT01:8

for AFV being WeakAffSegm
for a, b, b9, b99 being Element of AFV st a,b9 // a,b99 & a,b // a,b99 & not b = b9 & not b = b99 holds
b9 = b99