theorem :: AFVECT0:8
for AFV being WeakAffVect
for a, b, c, d, b9 being Element of AFV st a,b // c,d & a,c // b9,d holds
b = b9