let AFV be WeakAffVect; :: thesis: for q, p, a being Element of AFV holds PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)
let q, p, a 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 Th42;
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 Th36; :: thesis: verum