theorem Th18: :: AFVECT0:18

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