let AFV be WeakAffVect; for a, p, q being Element of AFV holds PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)
let a, p, q be Element of AFV; PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)
Mid PSym (q,a),p, PSym (p,(PSym (q,a)))
by Def4;
then
Mid PSym (q,(PSym (q,a))), PSym (q,p), PSym (q,(PSym (p,(PSym (q,a)))))
by Th35;
then
PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),(PSym (q,(PSym (q,a)))))
by Def4;
hence
PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)
by Th29; verum