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