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 Th30; :: thesis: verum