let AFV be WeakAffVect; :: thesis: for a, b, p being Element of AFV holds a,b // PSym (p,b), PSym (p,a)
let a, b, p be Element of AFV; :: thesis: a,b // PSym (p,b), PSym (p,a)
( Mid a,p, PSym (p,a) & Mid b,p, PSym (p,b) ) by Def4;
hence a,b // PSym (p,b), PSym (p,a) by Th25; :: thesis: verum