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