for AFV being WeakAffVect
for a being Element of AFV holds a,a // a,a by Th1;