:: deftheorem Def3 defines Mid AFVECT0:def 3 :
for AFV being WeakAffVect
for a, b, c being Element of AFV holds
( Mid a,b,c iff a,b // b,c );