let AFV be WeakAffVect; :: thesis: for p, a being Element of AFV holds PSym (p,(PSym (p,a))) = a
let p, a be Element of AFV; :: thesis: PSym (p,(PSym (p,a))) = a
Mid a,p, PSym (p,a) by Def4;
then Mid PSym (p,a),p,a by Th21;
hence PSym (p,(PSym (p,a))) = a by Def4; :: thesis: verum