for AFV being WeakAffVect
for a, b, c, p being Element of AFV ex d being Element of AFV st PSym (a,(PSym (b,(PSym (c,p))))) = PSym (d,p)