for AFV being WeakAffVect
for a, b, p being Element of AFV holds
( MDist a,b iff MDist PSym (p,a), PSym (p,b) ) by Th30, Th33;