theorem :: AFVECT0:11

for AFV being WeakAffVect
for a, b, c, d, f, a9, b9, c9, d9, f9 being Element of AFV st a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 holds
a,f // a9,f9