:: deftheorem defines MDist AFVECT01:def 2 :
for AFV being WeakAffSegm
for a, b being Element of AFV holds
( MDist a,b iff ex p, p9 being Element of AFV st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) );