let AFV be WeakAffVect; :: thesis: for a, b, p being Element of AFV ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p)))
let a, b, p be Element of AFV; :: thesis: ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p)))
consider c being Element of AFV such that
A1: Mid a,c,b by Th19;
PSym (b,p) = PSym ((PSym (c,a)),p) by A1, Def4
.= PSym (c,(PSym (a,(PSym (c,p))))) by Th37 ;
then PSym (c,(PSym (b,p))) = PSym (a,(PSym (c,p))) by Th29;
hence ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p))) ; :: thesis: verum