let AFV be WeakAffVect; :: thesis: 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; :: thesis: 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; :: thesis: verum