let AFV be WeakAffVect; 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; 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; verum