let AFV be WeakAffVect; :: thesis: for a, p, b being Element of AFV ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p)))
let a, p, b 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 Th24;
PSym (b,p) = PSym ((PSym (c,a)),p) by A1, Def4
.= PSym (c,(PSym (a,(PSym (c,p))))) by Th44 ;
then PSym (c,(PSym (b,p))) = PSym (a,(PSym (c,p))) by Th36;
hence ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p))) ; :: thesis: verum