let AFV be WeakAffVect; :: thesis: for a, p, q, r being Element of AFV holds PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))
let a, p, q, r 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 Th3, Th32;
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 Th3, Th32;
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 Th32;
then PSym (q,p), PSym (r,p) // p, PSym (r,(PSym (q,p))) by Th29;
then A3: p, PSym (r,(PSym (q,p))) // PSym (q,p), PSym (r,p) by Th3;
PSym (q,(PSym (r,p))),p // PSym (q,p), PSym (q,(PSym (q,(PSym (r,p))))) by Th32;
then PSym (q,(PSym (r,p))),p // PSym (q,p), PSym (r,p) by Th29;
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))) ;
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 Th28;
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 Th3, Th32;
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 Th3, Th32;
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 Th4, Th7; :: thesis: verum