theorem Th36: :: AFVECT0:36

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