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