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))
PSym q,(PSym r,p),p // PSym q,p, PSym q,(PSym q,(PSym r,p)) by Th39;
then A1: PSym q,(PSym r,p),p // PSym q,p, PSym r,p by Th36;
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 p, PSym r,(PSym q,p) // PSym q,p, PSym r,p by Th4;
then PSym q,(PSym r,p),p // p, PSym r,(PSym q,p) by A1, 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 A2: PSym p,(PSym q,(PSym r,p)) = PSym r,(PSym q,(PSym p,p)) by Th35;
A3: p,a // PSym r,a, PSym r,p by Th39;
PSym q,(PSym r,p), PSym q,(PSym r,a) // PSym r,a, PSym r,p by Th4, Th39;
then A4: p,a // PSym q,(PSym r,p), PSym q,(PSym r,a) by A3, 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 A5: PSym p,(PSym q,(PSym r,a)), PSym p,(PSym q,(PSym r,p)) // p,a by A4, Def1;
A6: p,a // PSym p,a, PSym p,p by Th39;
PSym q,(PSym p,p), PSym q,(PSym p,a) // PSym p,a, PSym p,p by Th4, Th39;
then A7: p,a // PSym q,(PSym p,p), PSym q,(PSym p,a) by A6, Def1;
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 PSym r,(PSym q,(PSym p,a)), PSym r,(PSym q,(PSym p,p)) // p,a by A7, 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 A2, A5, Def1;
hence PSym p,(PSym q,(PSym r,a)) = PSym r,(PSym q,(PSym p,a)) by Th5, Th8; :: thesis: verum