let AFV be WeakAffVect; :: thesis: for p, b being Element of AFV ex a being Element of AFV st PSym (p,a) = b
let p, b be Element of AFV; :: thesis: ex a being Element of AFV st PSym (p,a) = b
PSym (p,(PSym (p,b))) = b by Th36;
hence ex a being Element of AFV st PSym (p,a) = b ; :: thesis: verum