theorem Th39: :: AFVECT0:39

for AFV being WeakAffVect
for a, p, q, r being Element of AFV holds PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))