theorem :: AFVECT0:38

for AFV being WeakAffVect
for a, p, q being Element of AFV holds
( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) iff ( p = q or MDist p,q or MDist q, PSym (p,q) ) )