for AFV being WeakAffVect
for a, b being Element of AFV holds
( Mid a,b,b iff a = b ) by Def1, Th6;