for AFV being WeakAffVect
for a, b, p being Element of AFV holds
( PSym (p,a) = b iff a,p // p,b ) by Def3, Def4;