:: deftheorem defines MDist AFVECT0:def 2 :
for AFV being WeakAffVect
for a, b being Element of AFV holds
( MDist a,b iff ( a,b // b,a & a <> b ) );