let AFV be WeakAffVect; :: thesis: for p, q, r, a being Element of AFV holds PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))
let p, q, r, a be Element of AFV; :: thesis: PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))
( p,a // PSym (r,a), PSym (r,p) & PSym (q,(PSym (r,p))), PSym (q,(PSym (r,a))) // PSym (r,a), PSym (r,p) ) by Th4, Th39;
then A1: p,a // PSym (q,(PSym (r,p))), PSym (q,(PSym (r,a))) by Def1;
( p,a // PSym (p,a), PSym (p,p) & PSym (q,(PSym (p,p))), PSym (q,(PSym (p,a))) // PSym (p,a), PSym (p,p) ) by Th4, Th39;
then A2: p,a // PSym (q,(PSym (p,p))), PSym (q,(PSym (p,a))) by Def1;
PSym (q,p), PSym (r,p) // PSym (r,(PSym (r,p))), PSym (r,(PSym (q,p))) by Th39;
then PSym (q,p), PSym (r,p) // p, PSym (r,(PSym (q,p))) by Th36;
then A3: p, PSym (r,(PSym (q,p))) // PSym (q,p), PSym (r,p) by Th4;
PSym (q,(PSym (r,p))),p // PSym (q,p), PSym (q,(PSym (q,(PSym (r,p))))) by Th39;
then PSym (q,(PSym (r,p))),p // PSym (q,p), PSym (r,p) by Th36;
then PSym (q,(PSym (r,p))),p // p, PSym (r,(PSym (q,p))) by A3, Def1;
then Mid PSym (q,(PSym (r,p))),p, PSym (r,(PSym (q,p))) by Def3;
then PSym (p,(PSym (q,(PSym (r,p))))) = PSym (r,(PSym (q,p))) by Def4;
then A4: PSym (p,(PSym (q,(PSym (r,p))))) = PSym (r,(PSym (q,(PSym (p,p))))) by Th35;
PSym (r,(PSym (q,(PSym (p,a))))), PSym (r,(PSym (q,(PSym (p,p))))) // PSym (q,(PSym (p,p))), PSym (q,(PSym (p,a))) by Th4, Th39;
then A5: PSym (r,(PSym (q,(PSym (p,a))))), PSym (r,(PSym (q,(PSym (p,p))))) // p,a by A2, Def1;
PSym (p,(PSym (q,(PSym (r,a))))), PSym (p,(PSym (q,(PSym (r,p))))) // PSym (q,(PSym (r,p))), PSym (q,(PSym (r,a))) by Th4, Th39;
then PSym (p,(PSym (q,(PSym (r,a))))), PSym (p,(PSym (q,(PSym (r,p))))) // p,a by A1, Def1;
then PSym (p,(PSym (q,(PSym (r,a))))), PSym (p,(PSym (q,(PSym (r,p))))) // PSym (r,(PSym (q,(PSym (p,a))))), PSym (p,(PSym (q,(PSym (r,p))))) by A4, A5, Def1;
hence PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a))))) by Th5, Th8; :: thesis: verum