theorem Th37: :: AFVECT0:37

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