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