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